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: ( M is constant & the_value_of N = the_value_of M )

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 A1, FUNCT_1:12 ;

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

hence A9: M is constant ; :: thesis: the_value_of N = the_value_of M

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 A8, A3, FUNCT_1:def 12

.= the_value_of M by A9, YELLOW_6:def 8 ; :: thesis: verum

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: ( M is constant & the_value_of N = the_value_of M )

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 A1, FUNCT_1:12 ;

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

then A8:
the mapping of M is constant
by FUNCT_1:def 10;
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 A4, A5, A6, FUNCT_1:def 3;

thus the mapping of M . n1 = the mapping of N . (f . n1) by A1, A4, A5, FUNCT_1:13

.= the mapping of N . (f . n2) by A2, A7, FUNCT_1:def 10

.= the mapping of M . n2 by A1, A4, A6, FUNCT_1:13 ; :: thesis: verum

end;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 A4, A5, A6, FUNCT_1:def 3;

thus the mapping of M . n1 = the mapping of N . (f . n1) by A1, A4, A5, FUNCT_1:13

.= the mapping of N . (f . n2) by A2, A7, FUNCT_1:def 10

.= the mapping of M . n2 by A1, A4, A6, FUNCT_1:13 ; :: thesis: verum

hence A9: M is constant ; :: thesis: the_value_of N = the_value_of M

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 A8, A3, FUNCT_1:def 12

.= the_value_of M by A9, YELLOW_6:def 8 ; :: thesis: verum