let it1, it2 be ManySortedSet of NAT ; :: thesis: ( ex myc being Function st
( it1 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) & ex myc being Function st
( it2 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) implies it1 = it2 )
given myc1 being Function such that A6: it1 = myc1 and
A7: myc1 . 0 = G and
A8: for k being Nat
for G being SimpleGraph st G = myc1 . k holds
myc1 . (k + 1) = Mycielskian G ; :: thesis: ( for myc being Function holds
( not it2 = myc or not myc . 0 = G or ex k being Nat ex G being SimpleGraph st
( G = myc . k & not myc . (k + 1) = Mycielskian G ) ) or it1 = it2 )
given myc2 being Function such that A9: it2 = myc2 and
A10: myc2 . 0 = G and
A11: for k being Nat
for G being SimpleGraph st G = myc2 . k holds
myc2 . (k + 1) = Mycielskian G ; :: thesis: it1 = it2
defpred S1[ Nat] means ( myc1 . $1 is SimpleGraph & myc1 . $1 = myc2 . $1 );
A12: S1[ 0 ] by A7, A10;
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A14: S1[k] ; :: thesis: S1[k + 1]
reconsider H = myc1 . k as SimpleGraph by A14;
myc1 . (k + 1) = Mycielskian H by A8;
hence myc1 . (k + 1) is SimpleGraph ; :: thesis: myc1 . (k + 1) = myc2 . (k + 1)
thus myc1 . (k + 1) = Mycielskian H by A8
.= myc2 . (k + 1) by A14, A11 ; :: thesis: verum
end;
A15: for k being Nat holds S1[k] from NAT_1:sch 2(A12, A13);
 for i being object st i in NAT holds
myc1 . i = myc2 . i by A15;
hence it1 = it2 by A6, A9, PBOOLE:3; :: thesis: verum