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 A1: it1 = myc1 and
B1: myc1 . 0 = G and
C1: 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 A2: it2 = myc2 and
B2: myc2 . 0 = G and
C2: 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 );
P0: S₁[ 0 ] by B1, B2;
P1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IH: S₁[k] ; :: thesis: S₁[k + 1]
reconsider H = myc1 . k as SimpleGraph by IH;
myc1 . (k + 1) = Mycielskian H by C1;
hence myc1 . (k + 1) is SimpleGraph ; :: thesis: myc1 . (k + 1) = myc2 . (k + 1)
thus myc1 . (k + 1) = Mycielskian H by C1
.= myc2 . (k + 1) by IH, C2 ; :: thesis: verum

end;

D: for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
for i being set st i in NAT holds
myc1 . i = myc2 . i by D;
hence it1 = it2 by A1, A2, PBOOLE:3; :: thesis: verum