let L be non empty RelStr ; :: thesis: for N being constant net of L
for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )

let N be constant net of L; :: thesis: for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )

let M be subnet of N; :: thesis:
consider f being Function of M,N such that
A1: the mapping of M = the mapping of N * f and
for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p by YELLOW_6:def 9;
set y = the Element of dom the mapping of M;
A2: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
then A3: the_value_of the mapping of N = the mapping of N . (f . the Element of dom the mapping of M) by FUNCT_1:def 12
.= the mapping of M . the Element of dom the mapping of M by ;
A4: dom f = the carrier of M by FUNCT_2:def 1;
for n1, n2 being object st n1 in dom the mapping of M & n2 in dom the mapping of M holds
the mapping of M . n1 = the mapping of M . n2
proof
let n1, n2 be object ; :: thesis: ( n1 in dom the mapping of M & n2 in dom the mapping of M implies the mapping of M . n1 = the mapping of M . n2 )
assume that
A5: n1 in dom the mapping of M and
A6: n2 in dom the mapping of M ; :: thesis: the mapping of M . n1 = the mapping of M . n2
A7: ( f . n1 in rng f & f . n2 in rng f ) by ;
thus the mapping of M . n1 = the mapping of N . (f . n1) by
.= the mapping of N . (f . n2) by
.= the mapping of M . n2 by ; :: thesis: verum
end;
then A8: the mapping of M is constant by FUNCT_1:def 10;
hence A9: M is constant ; :: thesis:
thus the_value_of N = the_value_of the mapping of N by YELLOW_6:def 8
.= the_value_of the mapping of M by
.= the_value_of M by ; :: thesis: verum