let T be non empty 1-sorted ; :: thesis: for N being constant net of T
for i being Element of N holds N . i = the_value_of N
let N be constant net of T; :: thesis: for i being Element of N holds N . i = the_value_of N
let i be Element of N; :: thesis: N . i = the_value_of N
dom the mapping of N = the carrier of N by FUNCT_2:def 1;
hence N . i = the_value_of the mapping of N by FUNCT_1:def 12
.= the_value_of N by Def8 ;
:: thesis: verum