let l be Nat; :: thesis: l ! >= l
defpred S1[ Nat] means $1 ! >= $1;
A1: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume A2: l ! >= l ; :: thesis: S1[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 S1[l + 1] ; :: thesis: verum
end;
A5: S1[ 0 ] ;
for l being Nat holds S1[l] from NAT_1:sch 2(A5, A1);
 hence l ! >= l ; :: thesis: verum