set A = F₁();
A6: ex n being Nat st F₂() in (ElementaryInstructions F₁()) |^ n by Th79;
defpred S₁[ Nat] means for I being Element of F₁() st I in (ElementaryInstructions F₁()) |^ $1 holds
P₁[I];
(ElementaryInstructions F₁()) |^ 0 = ElementaryInstructions F₁() by Th18;
then A7: S₁[ 0 ] by A1;

A8: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let I be Element of F₁(); :: thesis: ( I in (ElementaryInstructions F₁()) |^ (n + 1) implies P₁[I] )
assume A10: I in (ElementaryInstructions F₁()) |^ (n + 1) ; :: thesis: P₁[I]

per cases ( I in (ElementaryInstructions F₁()) |^ n or I = EmptyIns F₁() or ex I1, I2 being Element of F₁() st
( I = I1 \; I2 & I1 in (ElementaryInstructions F₁()) |^ n & I2 in (ElementaryInstructions F₁()) |^ n ) or ex C, I1, I2 being Element of F₁() st
( I = if-then-else (C,I1,I2) & C in (ElementaryInstructions F₁()) |^ n & I1 in (ElementaryInstructions F₁()) |^ n & I2 in (ElementaryInstructions F₁()) |^ n ) or ex C, J being Element of F₁() st
( I = while (C,J) & C in (ElementaryInstructions F₁()) |^ n & J in (ElementaryInstructions F₁()) |^ n ) ) by A10, Th77;

suppose I in (ElementaryInstructions F₁()) |^ n ; :: thesis: P₁[I]

hence P₁[I] by A9; :: thesis: verum

end;

suppose I = EmptyIns F₁() ; :: thesis: P₁[I]

hence P₁[I] by A2; :: thesis: verum

end;

suppose ex I1, I2 being Element of F₁() st
( I = I1 \; I2 & I1 in (ElementaryInstructions F₁()) |^ n & I2 in (ElementaryInstructions F₁()) |^ n ) ; :: thesis: P₁[I]

then consider I1, I2 being Element of F₁() such that
A11: I = I1 \; I2 and
A12: I1 in (ElementaryInstructions F₁()) |^ n and
A13: I2 in (ElementaryInstructions F₁()) |^ n ;
A14: P₁[I1] by A9, A12;
P₁[I2] by A9, A13;
hence P₁[I] by A3, A11, A14; :: thesis: verum

end;

suppose ex C, I1, I2 being Element of F₁() st
( I = if-then-else (C,I1,I2) & C in (ElementaryInstructions F₁()) |^ n & I1 in (ElementaryInstructions F₁()) |^ n & I2 in (ElementaryInstructions F₁()) |^ n ) ; :: thesis: P₁[I]

then consider C, I1, I2 being Element of F₁() such that
A15: I = if-then-else (C,I1,I2) and
A16: C in (ElementaryInstructions F₁()) |^ n and
A17: I1 in (ElementaryInstructions F₁()) |^ n and
A18: I2 in (ElementaryInstructions F₁()) |^ n ;
A19: P₁[C] by A9, A16;
A20: P₁[I1] by A9, A17;
P₁[I2] by A9, A18;
hence P₁[I] by A4, A15, A19, A20; :: thesis: verum

end;

suppose ex C, J being Element of F₁() st
( I = while (C,J) & C in (ElementaryInstructions F₁()) |^ n & J in (ElementaryInstructions F₁()) |^ n ) ; :: thesis: P₁[I]

then consider C, J being Element of F₁() such that
A21: I = while (C,J) and
A22: C in (ElementaryInstructions F₁()) |^ n and
A23: J in (ElementaryInstructions F₁()) |^ n ;
A24: P₁[C] by A9, A22;
P₁[J] by A9, A23;
hence P₁[I] by A5, A21, A24; :: thesis: verum

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A8);
hence P₁[F₂()] by A6; :: thesis: verum