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