let G1, H1, G2, 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: ( len <*3*> = 1 & dom <*3*> = {1} ) by FINSEQ_1:4, FINSEQ_1:56, FINSEQ_1:def 8;
A2: ( dom (G1 '&' G2) = Seg (len (G1 '&' G2)) & dom G1 = Seg (len G1) & dom G2 = Seg (len G2) & dom (H1 '&' H2) = Seg (len (H1 '&' H2)) & dom H1 = Seg (len H1) & dom H2 = Seg (len H2) ) by FINSEQ_1:def 3;
A3: ( len (<*3*> ^ G1) = 1 + (len G1) & len (<*3*> ^ H1) = 1 + (len H1) ) by A1, FINSEQ_1:35;
then A4: ( len (G1 '&' G2) = (1 + (len G1)) + (len G2) & len (H1 '&' H2) = (1 + (len H1)) + (len H2) ) by FINSEQ_1:35;
A5: ( dom (<*3*> ^ G1) = Seg (1 + (len G1)) & dom (<*3*> ^ H1) = Seg (1 + (len H1)) ) by A3, FINSEQ_1:def 3;
assume A6: ( G1 = H1 / x,y & G2 = H2 / x,y ) ; :: thesis: G1 '&' G2 = (H1 '&' H2) / x,y
then A7: ( dom G1 = dom H1 & dom G2 = dom H2 ) by Def4;
then A8: ( len G1 = len H1 & len G2 = len H2 ) by FINSEQ_3:31;
then A9: ( dom ((H1 '&' H2) / x,y) = dom (G1 '&' G2) & dom ((H1 '&' H2) / x,y) = dom (H1 '&' H2) ) by A2, A4, Def4;

now

let a be set ; :: thesis: ( a in dom ((H1 '&' H2) / x,y) implies (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a )
assume A10: 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 A9;

A11: now

assume A12: i in dom (<*3*> ^ G1) ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a
then A13: ( (G1 '&' G2) . i = (<*3*> ^ G1) . i & (H1 '&' H2) . i = (<*3*> ^ H1) . i ) by A5, A8, FINSEQ_1:def 7;

A14: now

assume i in {1} ; :: thesis: ((H1 '&' H2) / x,y) . a = (G1 '&' G2) . a
then ( i = 1 & (H1 '&' H2) . 1 = 3 & x <> 3 ) by Th148, TARSKI:def 1, ZF_LANG:33;
then ( ((H1 '&' H2) / x,y) . i = 3 & (G1 '&' G2) . i = 3 ) by A9, A10, Def4, ZF_LANG:33;
hence ((H1 '&' H2) / x,y) . a = (G1 '&' G2) . a ; :: thesis: verum

end;

now

given j being Nat such that A15: ( j in dom G1 & i = 1 + j ) ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a
( G1 . j = (G1 '&' G2) . i & H1 . j = (H1 '&' H2) . i & j in dom H1 ) by A1, A7, A13, A15, FINSEQ_1:def 7;
then ( ( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) & ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) & ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / x,y) . a = (H1 '&' H2) . a ) & ( (H1 '&' H2) . a = x implies ((H1 '&' H2) / x,y) . a = y ) ) by A6, A9, A10, Def4;
hence (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a ; :: thesis: verum

end;

hence (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a by A1, A12, A14, FINSEQ_1:38; :: thesis: verum

end;

now

given j being Nat such that A16: ( j in dom G2 & i = (1 + (len G1)) + j ) ; :: thesis: (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a
( G2 . j = (G1 '&' G2) . i & H2 . j = (H1 '&' H2) . i & j in dom H2 ) by A2, A3, A8, A16, FINSEQ_1:def 7;
then ( ( (H1 '&' H2) . a <> x or (H1 '&' H2) . a = x ) & ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / x,y) . a = (H1 '&' H2) . a ) & ( (H1 '&' H2) . a = x implies ((H1 '&' H2) / x,y) . a = y ) & ( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) & ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) ) by A6, A9, A10, Def4;
hence (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a ; :: thesis: verum

end;

hence (G1 '&' G2) . a = ((H1 '&' H2) / x,y) . a by A3, A9, A10, A11, FINSEQ_1:38; :: thesis: verum

end;

hence G1 '&' G2 = (H1 '&' H2) / x,y by A9, FUNCT_1:9; :: thesis: verum