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