defpred S₁[ Nat] means Prod_real_n . $1 = $1 ! ;
A1: S₁[ 0 ] by Def2, NEWTON:12;

A2: now :: thesis: for l being Nat st S₁[l] holds
S₁[l + 1]

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A3: S₁[l] ; :: thesis: S₁[l + 1]
Prod_real_n . (l + 1) = (Prod_real_n . l) * (l + 1) by Def2
.= (l + 1) ! by A3, NEWTON:15 ;
hence S₁[l + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for b₁ being set holds
( b₁ = n ! iff b₁ = Prod_real_n . n ) ; :: thesis: verum