let s, t be Nat; :: thesis: (s ! ) * (t ! ) <> 0
A1: t ! <> 0 by Th23;
s ! <> 0 by Th23;
hence (s ! ) * (t ! ) <> 0 by A1; :: thesis: verum