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
<*1,2*> . 1 = 1 by FINSEQ_1:44;
hence not <*1,2*> . 1 = <*1,2*> . 2 by FINSEQ_1:44; :: thesis: verum