let G be finite SimpleGraph; :: thesis: for n being Nat holds order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1
let n be Nat; :: thesis: order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1
set g = order G;
set MG = MycielskianSeq G;
defpred S₁[ Nat] means order ((MycielskianSeq G) . $1) = (((2 |^ $1) * (order G)) + (2 |^ $1)) - 1;
A1: S₁[ 0 ]

proof

thus order ((MycielskianSeq G) . 0) = ((order G) + 1) - 1 by Th113
.= ((1 * (order G)) + (2 |^ 0)) - 1 by NEWTON:4
.= (((2 |^ 0) * (order G)) + (2 |^ 0)) - 1 by NEWTON:4 ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus order ((MycielskianSeq G) . (n + 1)) = order (Mycielskian ((MycielskianSeq G) . n)) by Th115
.= (2 * ((((2 |^ n) * (order G)) + (2 |^ n)) - 1)) + 1 by A3, Th89
.= ((((2 * (2 |^ n)) * (order G)) + (2 * (2 |^ n))) - (2 * 1)) + 1
.= ((((2 |^ (n + 1)) * (order G)) + (2 * (2 |^ n))) - (2 * 1)) + 1 by NEWTON:6
.= ((((2 |^ (n + 1)) * (order G)) + (2 |^ (n + 1))) - 2) + 1 by NEWTON:6
.= (((2 |^ (n + 1)) * (order G)) + (2 |^ (n + 1))) - 1 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1 ; :: thesis: verum