let f be Function; :: thesis: for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let T be non empty array of O; :: thesis: for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let p, q be Element of dom T; :: thesis: ( p in q & f = (T,p,q) incl implies for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 ) )
assume A1: ( p in q & f = (T,p,q) incl ) ; :: thesis: for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
then A2: p <> q ;
let x1, x2, y1, y2 be Element of dom T; :: thesis: ( x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume that
A3: ( x1 in y1 & x2 in y2 ) and
A4: f . (x1,y1) = f . (x2,y2) ; :: thesis: ( x1 = x2 & y1 = y2 )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
per cases ( ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) or ( x1 = p & y1 in q ) or ( x1 = p & y1 = q ) or ( p in x1 & y1 = q ) or ( x1 in p & y1 = p ) or ( x1 in p & y1 = q ) or ( x1 = p & q in y1 ) or ( x1 = q & q in y1 ) ) by A1, A3, Th2;
suppose A5: ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A6: f . (x1,y1) = [x1,y1] by A1, Th67;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,q] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [p,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A7: ( x1 = p & y1 in q ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A8: f . (x1,y1) = [x1,y1] by A1, A3, Th69;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,p] & x2 <> p ) by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A2, A7, A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; :: thesis: verum
end;
suppose A9: S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [p,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A7, A9, A4, A8, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A10: ( x1 = p & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A11: f . (x1,y1) = [x1,y1] by A1, Th66;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A12: ( p in x1 & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A13: f . (x1,y1) = [x1,y1] by A1, A3, Th69;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose A14: S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,q] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A14, A12, A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose A15: S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A15, A12, A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A16: ( x1 in p & y1 = p ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A17: f . (x1,y1) = [x1,q] by A1, Th68;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose A18: S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A18, A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose A19: S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,q] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A19, A16, A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A2, A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose A20: S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A16, A20, A4, A17, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [p,y2] & x1 <> p ) by A16, A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A21: ( x1 in p & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A22: f . (x1,y1) = [x1,p] by A1, Th68;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose A23: S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A23, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,q] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A2, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose A24: S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A24, A21, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose A25: S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & x1 <> p ) by A21, A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A25, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose A26: S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A26, A2, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A1, A21, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose A27: S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A2, A27, A4, A22, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [p,y2] & x1 <> p ) by A21, A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A4, A22, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A28: ( x1 = p & q in y1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A29: f . (x1,y1) = [q,y1] by A1, Th70;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose A30: S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A30, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose A31: S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,q] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A1, A31, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,p] by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A1, A28, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose A32: S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A2, A32, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose A33: S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A33, A28, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; :: thesis: verum
end;
suppose S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [p,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A2, A4, A29, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
suppose A34: ( x1 = q & q in y1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then A35: f . (x1,y1) = [p,y1] by A1, Th70;
per cases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose A36: S1[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, Th67;
hence ( x1 = x2 & y1 = y2 ) by A36, A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose S2[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,q] & p <> x2 ) by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose S3[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,p] & p <> x2 ) by A1, Th68;
hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose A37: S4[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A34, A37, A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose S5[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & y1 <> y2 ) by A34, A1, Th66;
hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose S6[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [q,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A2, A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose S7[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( f . (x2,y2) = [x2,y2] & y2 <> y1 ) by A34, A1, A3, Th69;
hence ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; :: thesis: verum
end;
suppose A38: S8[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )
then f . (x2,y2) = [p,y2] by A1, Th70;
hence ( x1 = x2 & y1 = y2 ) by A38, A34, A4, A35, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
end;