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 )
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:4, FINSEQ_3:29; :: thesis: not <*1,2*> . 1 = <*1,2*> . 2
<*1,2*> . 1 = 1 by FINSEQ_1:61;
hence not <*1,2*> . 1 = <*1,2*> . 2 by FINSEQ_1:61; :: thesis: verum