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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose S₁[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 S₂[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 S₃[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 S₄[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 S₅[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 S₆[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 S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose S₁[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 S₂[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 S₃[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 S₄[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 S₅[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 S₆[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 S₇[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: S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose S₁[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 S₂[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 S₃[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 S₄[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 S₅[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 S₆[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 S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose S₁[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: S₂[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: S₃[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 S₄[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 S₅[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 S₆[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 S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose A18: S₁[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: S₂[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 S₃[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 S₄[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 S₅[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 S₆[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: S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose A23: S₁[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 S₂[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: S₃[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: S₄[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: S₅[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 S₆[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: S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose A30: S₁[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: S₂[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 S₃[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 S₄[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: S₅[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: S₆[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 S₇[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 S₈[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 ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by A1, A3, Th2;

suppose A36: S₁[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 S₂[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 S₃[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: S₄[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 S₅[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 S₆[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 S₇[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: S₈[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;