let G be SimpleGraph; :: thesis: (MycielskianSeq G) . 0 = G
consider myc being Function such that
A1: MycielskianSeq G = myc and
A2: myc . 0 = G and
for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G by Def26;
thus (MycielskianSeq G) . 0 = G by A1, A2; :: thesis: verum