let x1, x2, y1, y2 be set ; :: thesis: ( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
assume {[x1,y1],[x2,y2]} is FinSequence ; :: thesis: ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
then reconsider p = {[x1,y1],[x2,y2]} as FinSequence ;
A1: dom p = {x1,x2} by RELAT_1:10;
then A2: x1 in dom p by TARSKI:def 2;
A3: x2 in dom p by A1, TARSKI:def 2;
A4: [x1,y1] in p by TARSKI:def 2;
A5: [x2,y2] in p by TARSKI:def 2;
A6: p . x1 = y1 by A4, FUNCT_1:1;
A7: p . x2 = y2 by A5, FUNCT_1:1;
A8: dom p = Seg (len p) by Def3;
A9: len p <= 1 + 1 by CARD_2:50;
A10: len p >= 0 + 1 by NAT_1:13;
A11: now :: thesis: ( len p = 1 implies ( x1 = 1 & x2 = 1 & y1 = y2 ) )
assume len p = 1 ; :: thesis: ( x1 = 1 & x2 = 1 & y1 = y2 )
hence ( x1 = 1 & x2 = 1 ) by A2, A3, A8, Th2, TARSKI:def 1; :: thesis: y1 = y2
hence y1 = y2 by A5, A6, FUNCT_1:1; :: thesis: verum
end;
now :: thesis: ( not len p = 2 or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
assume A12: len p = 2 ; :: thesis: ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
A13: ( x1 = x2 implies p = {[x1,y1]} ) by A6, A7, ENUMSET1:29;
( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 1 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A3, A8, A12, Th2, TARSKI:def 2;
hence ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A12, A13, CARD_1:30; :: thesis: verum
end;
hence ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A9, A10, A11, NAT_1:9; :: thesis: verum