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