let R1, R2 be non empty reflexive RelStr ; :: thesis: for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let X be non empty set ; :: thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N1 be net of R1; :: thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N2 be net of R2; :: thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2 )
assume A1: N1 = N2 ; :: thesis: for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J1 be net_set of the carrier of N1,R1; :: thesis: for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J2 be net_set of the carrier of N2,R2; :: thesis: ( J1 = J2 implies Iterated J1 = Iterated J2 )
assume A2: J1 = J2 ; :: thesis: Iterated J1 = Iterated J2
A3: RelStr(# the carrier of (Iterated J1), the InternalRel of (Iterated J1) #) = [:N1,(product J1):] by YELLOW_6:def 13;
A4: RelStr(# the carrier of (Iterated J2), the InternalRel of (Iterated J2) #) = [:N2,(product J2):] by YELLOW_6:def 13;
set f = the mapping of (Iterated J1);
set g = the mapping of (Iterated J2);
A5: dom the mapping of (Iterated J1) = the carrier of (Iterated J2) by A1, A2, A3, A4, FUNCT_2:def 1
.= dom the mapping of (Iterated J2) by FUNCT_2:def 1 ;
for x being object st x in dom the mapping of (Iterated J1) holds
the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x

proof

let x be object ; :: thesis: ( x in dom the mapping of (Iterated J1) implies the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x )
assume x in dom the mapping of (Iterated J1) ; :: thesis: the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x
then x in the carrier of (Iterated J1) ;
then x in [: the carrier of N1, the carrier of (product J1):] by A3, YELLOW_3:def 2;
then consider x1 being Element of N1, x2 being Element of (product J1) such that
A6: x = [x1,x2] by DOMAIN_1:1;
reconsider y1 = x1 as Element of N2 by A1;
reconsider y2 = x2 as Element of (product J2) by A1, A2;
thus the mapping of (Iterated J1) . x = the mapping of (Iterated J1) . (x1,x2) by A6
.= the mapping of (J1 . x1) . (x2 . x1) by YELLOW_6:def 13
.= the mapping of (J2 . y1) . (y2 . y1) by A2
.= the mapping of (Iterated J2) . (y1,y2) by YELLOW_6:def 13
.= the mapping of (Iterated J2) . x by A6 ; :: thesis: verum

end;

then the mapping of (Iterated J1) = the mapping of (Iterated J2) by A5, FUNCT_1:2;
hence Iterated J1 = Iterated J2 by A1, A2, A3, A4; :: thesis: verum