2 ! = 1 * 2 by FINSEQ_2:52, RVSUM_1:99;
hence 2 ! = 2 ; :: thesis: verum