let L be non empty RelStr ; 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; for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )
let M be subnet of N; ( 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
let n1,
n2 be
object ;
( 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
;
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
;
verum
end;
then A8:
the mapping of M is constant
by FUNCT_1:def 10;
hence A9:
M is constant
; 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
; verum