let x1, x2, y1, y2 be object ; :: thesis: ( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
thus ( {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2 ) :: thesis: ( ( x1 = x2 implies y1 = y2 ) implies {[x1,y1],[x2,y2]} is Function )
proof
A1: ( [x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in {[x1,y1],[x2,y2]} ) by TARSKI:def 2;
assume {[x1,y1],[x2,y2]} is Function ; :: thesis: ( not x1 = x2 or y1 = y2 )
hence ( not x1 = x2 or y1 = y2 ) by A1, FUNCT_1:def 1; :: thesis: verum
end;
assume A2: ( x1 = x2 implies y1 = y2 ) ; :: thesis: {[x1,y1],[x2,y2]} is Function
now :: thesis: ( ( for p being object st p in {[x1,y1],[x2,y2]} holds
ex x, y being object st [x,y] = p ) & ( for x, z1, z2 being object st [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} holds
z1 = z2 ) )
thus for p being object st p in {[x1,y1],[x2,y2]} holds
ex x, y being object st [x,y] = p :: thesis: for x, z1, z2 being object st [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} holds
z1 = z2
proof
let p be object ; :: thesis: ( p in {[x1,y1],[x2,y2]} implies ex x, y being object st [x,y] = p )
assume p in {[x1,y1],[x2,y2]} ; :: thesis: ex x, y being object st [x,y] = p
then ( p = [x1,y1] or p = [x2,y2] ) by TARSKI:def 2;
hence ex x, y being object st [x,y] = p ; :: thesis: verum
end;
let x, z1, z2 be object ; :: thesis: ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} implies z1 = z2 )
A3: ( ( not ( [x,z1] = [x1,y1] & [x,z2] = [x1,y1] ) & not ( [x,z1] = [x2,y2] & [x,z2] = [x2,y2] ) ) or ( z1 = y1 & z2 = y1 ) or ( z1 = y2 & z2 = y2 ) ) by XTUPLE_0:1;
A4: now :: thesis: ( ( ( [x,z1] = [x1,y1] & [x,z2] = [x2,y2] ) or ( [x,z1] = [x2,y2] & [x,z2] = [x1,y1] ) ) implies z1 = z2 )
assume A5: ( ( [x,z1] = [x1,y1] & [x,z2] = [x2,y2] ) or ( [x,z1] = [x2,y2] & [x,z2] = [x1,y1] ) ) ; :: thesis: z1 = z2
then ( x = x1 & x = x2 ) by XTUPLE_0:1;
hence z1 = z2 by A2, A5, XTUPLE_0:1; :: thesis: verum
end;
assume ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} ) ; :: thesis: z1 = z2
hence z1 = z2 by A3, A4, TARSKI:def 2; :: thesis: verum
end;
hence {[x1,y1],[x2,y2]} is Function by FUNCT_1:def 1; :: thesis: verum