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 S₁[ Nat] means ( myc1 . $1 is SimpleGraph & myc1 . $1 = myc2 . $1 );
A12: S₁[ 0 ] by A7, A10;
A13: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: S₁[k] ; :: thesis: S₁[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 S₁[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