2 ! = 1 * 2 by FINSEQ_2:61, RVSUM_1:129;
hence 2 ! = 2 ; :: thesis: verum