take <*1,2*> ; :: thesis: not <*1,2*> is constant
take 1 ; :: according to SEQM_3:def 10 :: thesis: ex b₁ being set st
( 1 in dom <*1,2*> & b₁ in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . b₁ )
take 2 ; :: thesis: ( 1 in dom <*1,2*> & 2 in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . 2 )
A1: 1 in {1,2} by TARSKI:def 2;
2 in {1,2} by TARSKI:def 2;
hence ( 1 in dom <*1,2*> & 2 in dom <*1,2*> ) by A1, FINSEQ_1:2, FINSEQ_1:89; :: thesis: not <*1,2*> . 1 = <*1,2*> . 2
thus not <*1,2*> . 1 = <*1,2*> . 2 ; :: thesis: verum