let G1, G2, H1, H2 be ZF-formula; :: thesis: for x, y being Variable st G1 = H1 / (x,y) & G2 = H2 / (x,y) holds
G1 '&' G2 = (H1 '&' H2) / (x,y)
let x, y be Variable; :: thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) )
set N = (H1 '&' H2) / (x,y);
A1: dom <*3*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
A2: ( dom (G1 '&' G2) = Seg (len (G1 '&' G2)) & dom (H1 '&' H2) = Seg (len (H1 '&' H2)) ) by FINSEQ_1:def 3;
A3: len <*3*> = 1 by FINSEQ_1:39;
then A4: len (<*3*> ^ G1) = 1 + (len G1) by FINSEQ_1:22;
then A5: len (G1 '&' G2) = (1 + (len G1)) + (len G2) by FINSEQ_1:22;
A6: len (<*3*> ^ H1) = 1 + (len H1) by A3, FINSEQ_1:22;
then A7: len (H1 '&' H2) = (1 + (len H1)) + (len H2) by FINSEQ_1:22;
A8: dom (<*3*> ^ H1) = Seg (1 + (len H1)) by A6, FINSEQ_1:def 3;
A9: dom ((H1 '&' H2) / (x,y)) = dom (H1 '&' H2) by Def3;
assume that
A10: G1 = H1 / (x,y) and
A11: G2 = H2 / (x,y) ; :: thesis: G1 '&' G2 = (H1 '&' H2) / (x,y)
A12: dom G1 = dom H1 by A10, Def3;
then A13: len G1 = len H1 by FINSEQ_3:29;
A14: dom G2 = dom H2 by A11, Def3;
then len G2 = len H2 by FINSEQ_3:29;
then A15: dom ((H1 '&' H2) / (x,y)) = dom (G1 '&' G2) by A2, A5, A7, A13, Def3;
A16: dom (<*3*> ^ G1) = Seg (1 + (len G1)) by A4, FINSEQ_1:def 3;
now :: thesis: for a being object st a in dom ((H1 '&' H2) / (x,y)) holds
(G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
let a be object ; :: thesis: ( a in dom ((H1 '&' H2) / (x,y)) implies (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a )
assume A17: a in dom ((H1 '&' H2) / (x,y)) ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
then reconsider i = a as Element of NAT by A15;
A18: now :: thesis: ( i in dom (<*3*> ^ G1) implies (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a )
A19: now :: thesis: ( i in {1} implies ((H1 '&' H2) / (x,y)) . a = (G1 '&' G2) . a )
assume i in {1} ; :: thesis: ((H1 '&' H2) / (x,y)) . a = (G1 '&' G2) . a
then A20: i = 1 by TARSKI:def 1;
( (H1 '&' H2) . 1 = 3 & x <> 3 ) by Th135, ZF_LANG:16;
then ((H1 '&' H2) / (x,y)) . i = 3 by A9, A17, A20, Def3;
hence ((H1 '&' H2) / (x,y)) . a = (G1 '&' G2) . a by A20, ZF_LANG:16; :: thesis: verum
end;
assume A21: i in dom (<*3*> ^ G1) ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
then A22: ( (G1 '&' G2) . i = (<*3*> ^ G1) . i & (H1 '&' H2) . i = (<*3*> ^ H1) . i ) by A16, A8, A13, FINSEQ_1:def 7;
now :: thesis: ( ex j being Nat st
( j in dom G1 & i = 1 + j ) implies (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a )
A23: ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / (x,y)) . a = (H1 '&' H2) . a ) by A9, A17, Def3;
given j being Nat such that A24: j in dom G1 and
A25: i = 1 + j ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
A26: ( G1 . j = (G1 '&' G2) . i & H1 . j = (H1 '&' H2) . i ) by A3, A12, A22, A24, A25, FINSEQ_1:def 7;
then A27: ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) by A10, A12, A24, Def3;
( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) by A10, A12, A24, A26, Def3;
hence (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A9, A17, A27, A23, Def3; :: thesis: verum
end;
hence (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A3, A1, A21, A19, FINSEQ_1:25; :: thesis: verum
end;
now :: thesis: ( ex j being Nat st
( j in dom G2 & i = (1 + (len G1)) + j ) implies (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a )
A28: ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / (x,y)) . a = (H1 '&' H2) . a ) by A9, A17, Def3;
given j being Nat such that A29: j in dom G2 and
A30: i = (1 + (len G1)) + j ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
A31: ( G2 . j = (G1 '&' G2) . i & H2 . j = (H1 '&' H2) . i ) by A4, A6, A14, A13, A29, A30, FINSEQ_1:def 7;
then A32: ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) by A11, A14, A29, Def3;
( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) by A11, A14, A29, A31, Def3;
hence (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A9, A17, A28, A32, Def3; :: thesis: verum
end;
hence (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A4, A15, A17, A18, FINSEQ_1:25; :: thesis: verum
end;
hence G1 '&' G2 = (H1 '&' H2) / (x,y) by A15, FUNCT_1:2; :: thesis: verum