let T be non empty 1-sorted ; :: thesis: for N being constant net of constant
for i being Element of holds N . i = the_value_of N
let N be constant net of constant ; :: thesis: for i being Element of holds N . i = the_value_of N
let i be Element of ; :: 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 18
.= the_value_of N by Def10 ;
:: thesis: verum