take <*1,2*> ; :: thesis: not <*1,2*> is constant
take 1 ; :: according to GOBOARD1:def 2 :: thesis: ex b₁ being Element of NAT 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 )
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
hence ( 1 in dom <*1,2*> & 2 in dom <*1,2*> ) by FINSEQ_1:4, FINSEQ_3:29; :: thesis: not <*1,2*> . 1 = <*1,2*> . 2
( <*1,2*> . 1 = 1 & <*1,2*> . 2 = 2 ) by FINSEQ_1:61;
hence not <*1,2*> . 1 = <*1,2*> . 2 ; :: thesis: verum