let n be Element of NAT ; :: thesis: VERUM <> prop n
A1: ( VERUM . 1 = 0 & (prop n) . 1 = 3 + n ) by FINSEQ_1:57;
assume not VERUM <> prop n ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum