let F, H be ZF-formula; :: thesis: for x, y, z, s being Variable st F = H / (x,y) & ( ( z = s & s <> x ) or ( z = y & s = x ) ) holds
All (z,F) = (All (s,H)) / (x,y)
let x, y, z, s be Variable; :: thesis: ( F = H / (x,y) & ( ( z = s & s <> x ) or ( z = y & s = x ) ) implies All (z,F) = (All (s,H)) / (x,y) )
set N = (All (s,H)) / (x,y);
A1: ( len <*4*> = 1 & 1 + 1 = 2 ) by FINSEQ_1:39;
len <*s*> = 1 by FINSEQ_1:39;
then A2: len (<*4*> ^ <*s*>) = 2 by A1, FINSEQ_1:22;
then A3: dom (<*4*> ^ <*s*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
len (All (s,H)) = 2 + (len H) by A2, FINSEQ_1:22;
then A4: dom (All (s,H)) = Seg (2 + (len H)) by FINSEQ_1:def 3;
A5: ( <*4*> ^ <*z*> = <*4,z*> & <*4*> ^ <*s*> = <*4,s*> ) by FINSEQ_1:def 9;
A6: dom ((All (s,H)) / (x,y)) = dom (All (s,H)) by Def3;
assume that
A7: F = H / (x,y) and
A8: ( ( z = s & s <> x ) or ( z = y & s = x ) ) ; :: thesis: All (z,F) = (All (s,H)) / (x,y)
A9: dom F = dom H by A7, Def3;
len <*z*> = 1 by FINSEQ_1:39;
then A10: len (<*4*> ^ <*z*>) = 2 by A1, FINSEQ_1:22;
then A11: dom (<*4*> ^ <*z*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;

A12: now :: thesis: for a being object st a in dom ((All (s,H)) / (x,y)) holds
(All (z,F)) . a = ((All (s,H)) / (x,y)) . a

let a be object ; :: thesis: ( a in dom ((All (s,H)) / (x,y)) implies (All (z,F)) . a = ((All (s,H)) / (x,y)) . a )
assume A13: a in dom ((All (s,H)) / (x,y)) ; :: thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
then reconsider a1 = a as Element of NAT by A6;

A14: now :: thesis: ( a in {1,2} implies (All (z,F)) . a = ((All (s,H)) / (x,y)) . a )

A15: ( x <> 4 & <*4,z*> . 1 = 4 ) by Th135;
assume A18: a in {1,2} ; :: thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
then A19: ( a = 1 or a = 2 ) by TARSKI:def 2;
( (All (z,F)) . a1 = <*4,z*> . a1 & (All (s,H)) . a1 = <*4,s*> . a1 ) by A11, A3, A5, A18, FINSEQ_1:def 7;
hence (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A8, A6, A13, A19, A15, Def3; :: thesis: verum

end;

now :: thesis: ( ex i being Nat st
( i in dom H & a1 = 2 + i ) implies (All (z,F)) . a = ((All (s,H)) / (x,y)) . a )

A20: ( (All (s,H)) . a <> x implies ((All (s,H)) / (x,y)) . a = (All (s,H)) . a ) by A6, A13, Def3;
given i being Nat such that A21: i in dom H and
A22: a1 = 2 + i ; :: thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
A23: ( (All (z,F)) . a = F . i & (All (s,H)) . a = H . i ) by A10, A2, A9, A21, A22, FINSEQ_1:def 7;
then A24: ( (All (s,H)) . a = x implies (All (z,F)) . a = y ) by A7, A21, Def3;
( (All (s,H)) . a <> x implies (All (z,F)) . a = (All (s,H)) . a ) by A7, A21, A23, Def3;
hence (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A6, A13, A24, A20, Def3; :: thesis: verum

end;

hence (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A2, A3, A6, A13, A14, FINSEQ_1:25; :: thesis: verum

end;

len (All (z,F)) = 2 + (len F) by A10, FINSEQ_1:22;
then dom (All (z,F)) = Seg (2 + (len F)) by FINSEQ_1:def 3;
then dom (All (s,H)) = dom (All (z,F)) by A4, A9, FINSEQ_3:29;
hence All (z,F) = (All (s,H)) / (x,y) by A6, A12, FUNCT_1:2; :: thesis: verum