let x1, x2, y1, y2, z1, z2 be Variable; :: thesis: ( (x1 '=' x2) / y1,y2 = z1 '=' z2 iff ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
set H = x1 '=' x2;
set Hz = z1 '=' z2;
set f = (x1 '=' x2) / y1,y2;
( x1 '=' x2 is being_equality & z1 '=' z2 is being_equality ) by ZF_LANG:16;
then A1: ( x1 '=' x2 is atomic & z1 '=' z2 is atomic ) by ZF_LANG:def 15;
then A2: ( len (x1 '=' x2) = 3 & len (z1 '=' z2) = 3 ) by ZF_LANG:27;
then A3: dom (x1 '=' x2) = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
A4: ( Var1 (x1 '=' x2) = x1 & Var2 (x1 '=' x2) = x2 & Var1 (z1 '=' z2) = z1 & Var2 (z1 '=' z2) = z2 ) by Th1;
then A5: ( (x1 '=' x2) . 1 = 0 & (x1 '=' x2) . 2 = x1 & (x1 '=' x2) . 3 = x2 & (z1 '=' z2) . 1 = 0 & (z1 '=' z2) . 2 = z1 & (z1 '=' z2) . 3 = z2 ) by A1, ZF_LANG:31, ZF_LANG:52;
thus ( not (x1 '=' x2) / y1,y2 = z1 '=' z2 or ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) :: thesis: ( ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) implies (x1 '=' x2) / y1,y2 = z1 '=' z2 )

proof

assume A6: (x1 '=' x2) / y1,y2 = z1 '=' z2 ; :: thesis: ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) )

per cases ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;

case ( x1 <> y1 & x2 <> y1 ) ; :: thesis: ( z1 = x1 & z2 = x2 )

then ( (x1 '=' x2) . 2 <> y1 & (x1 '=' x2) . 3 <> y1 & 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A1, A3, A4, ENUMSET1:def 1, ZF_LANG:52;
hence ( z1 = x1 & z2 = x2 ) by A5, A6, Def4; :: thesis: verum

end;

case ( x1 = y1 & x2 <> y1 ) ; :: thesis: ( z1 = y2 & z2 = x2 )

then ( (x1 '=' x2) . 2 = y1 & (x1 '=' x2) . 3 <> y1 & 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A1, A3, A4, ENUMSET1:def 1, ZF_LANG:52;
hence ( z1 = y2 & z2 = x2 ) by A5, A6, Def4; :: thesis: verum

end;

case ( x1 <> y1 & x2 = y1 ) ; :: thesis: ( z1 = x1 & z2 = y2 )

then ( (x1 '=' x2) . 2 <> y1 & (x1 '=' x2) . 3 = y1 & 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A1, A3, A4, ENUMSET1:def 1, ZF_LANG:52;
hence ( z1 = x1 & z2 = y2 ) by A5, A6, Def4; :: thesis: verum

end;

case ( x1 = y1 & x2 = y1 ) ; :: thesis: ( z1 = y2 & z2 = y2 )

then ( (x1 '=' x2) . 2 = y1 & (x1 '=' x2) . 3 = y1 & 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A1, A3, A4, ENUMSET1:def 1, ZF_LANG:52;
hence ( z1 = y2 & z2 = y2 ) by A5, A6, Def4; :: thesis: verum

end;

end;

end;

A7: ( dom ((x1 '=' x2) / y1,y2) = dom (x1 '=' x2) & dom (x1 '=' x2) = Seg 3 & dom (z1 '=' z2) = Seg 3 ) by A2, Def4, FINSEQ_1:def 3;
A8: y1 <> 0 by Th148;

A9: now

assume A10: ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) ; :: thesis: (x1 '=' x2) / y1,y2 = z1 '=' z2

now

let a be set ; :: thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a )
assume A11: a in dom (x1 '=' x2) ; :: thesis: (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a
then ( a = 1 or a = 2 or a = 3 ) by A3, ENUMSET1:def 1;
hence (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a by A5, A8, A10, A11, Def4; :: thesis: verum

end;

hence (x1 '=' x2) / y1,y2 = z1 '=' z2 by A7, FUNCT_1:9; :: thesis: verum

end;

A12: now

assume A13: ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) ; :: thesis: (x1 '=' x2) / y1,y2 = z1 '=' z2

now

let a be set ; :: thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a )
assume A14: a in dom (x1 '=' x2) ; :: thesis: (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a
then ( a = 1 or a = 2 or a = 3 ) by A3, ENUMSET1:def 1;
hence (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a by A5, A8, A13, A14, Def4; :: thesis: verum

end;

hence (x1 '=' x2) / y1,y2 = z1 '=' z2 by A7, FUNCT_1:9; :: thesis: verum

end;

A15: now

assume A16: ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) ; :: thesis: (x1 '=' x2) / y1,y2 = z1 '=' z2

now

let a be set ; :: thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a )
assume A17: a in dom (x1 '=' x2) ; :: thesis: (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a
then ( a = 1 or a = 2 or a = 3 ) by A3, ENUMSET1:def 1;
hence (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a by A5, A8, A16, A17, Def4; :: thesis: verum

end;

hence (x1 '=' x2) / y1,y2 = z1 '=' z2 by A7, FUNCT_1:9; :: thesis: verum

end;

now

assume A18: ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ; :: thesis: (x1 '=' x2) / y1,y2 = z1 '=' z2

now

let a be set ; :: thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a )
assume A19: a in dom (x1 '=' x2) ; :: thesis: (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a
then ( a = 1 or a = 2 or a = 3 ) by A3, ENUMSET1:def 1;
hence (z1 '=' z2) . a = ((x1 '=' x2) / y1,y2) . a by A5, A8, A18, A19, Def4; :: thesis: verum

end;

hence (x1 '=' x2) / y1,y2 = z1 '=' z2 by A7, FUNCT_1:9; :: thesis: verum

end;

hence ( ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) implies (x1 '=' x2) / y1,y2 = z1 '=' z2 ) by A9, A12, A15; :: thesis: verum