let l be Nat; :: thesis: l ! >= l
defpred S₁[ Nat] means $1 ! >= $1;
A1: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A2: l ! >= l ; :: thesis: S₁[l + 1]
A3: (l !) * (l + 1) = (l + 1) ! by Th15;
( ( l = 0 & (l + 1) ! >= l + 1 ) or ( l >= 1 & (l + 1) ! >= l + 1 ) )

proof

per cases ( l = 0 or l >= 1 ) by NAT_1:14;

case l = 0 ; :: thesis: (l + 1) ! >= l + 1

hence (l + 1) ! >= l + 1 by FINSEQ_2:50; :: thesis: verum

end;

case A4: l >= 1 ; :: thesis: (l + 1) ! >= l + 1

(l + 1) ! >= (l + 1) * l by A2, A3, XREAL_1:64;
hence (l + 1) ! >= l + 1 by A4, Th34; :: thesis: verum

end;

end;

end;

hence S₁[l + 1] ; :: thesis: verum

end;

A5: S₁[ 0 ] ;
for l being Nat holds S₁[l] from NAT_1:sch 2(A5, A1);
hence l ! >= l ; :: thesis: verum