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;
( len <*4*> = 1 & len <*z*> = 1 & len <*s*> = 1 & 1 + 1 = 2 ) by FINSEQ_1:56;
then A1: ( len (<*4*> ^ <*z*>) = 2 & len (<*4*> ^ <*s*>) = 2 ) by FINSEQ_1:35;
then ( len (All z,F) = 2 + (len F) & len (All s,H) = 2 + (len H) ) by FINSEQ_1:35;
then A2: ( dom (All z,F) = Seg (2 + (len F)) & dom (All s,H) = Seg (2 + (len H)) & dom H = Seg (len H) & dom F = Seg (len F) ) by FINSEQ_1:def 3;
A3: ( dom (<*4*> ^ <*z*>) = {1,2} & dom (<*4*> ^ <*s*>) = {1,2} & <*4*> ^ <*z*> = <*4,z*> & <*4*> ^ <*s*> = <*4,s*> ) by A1, FINSEQ_1:4, FINSEQ_1:def 3, FINSEQ_1:def 9;
assume A4: ( F = H / x,y & ( ( z = s & s <> x ) or ( z = y & s = x ) ) ) ; :: thesis: All z,F = (All s,H) / x,y
then A5: dom F = dom H by Def4;
then A6: ( dom (All s,H) = dom (All z,F) & dom ((All s,H) / x,y) = dom (All s,H) ) by A2, Def4, FINSEQ_3:31;

now

let a be set ; :: thesis: ( a in dom ((All s,H) / x,y) implies (All z,F) . a = ((All s,H) / x,y) . a )
assume A7: 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;

A8: now

assume A9: a in {1,2} ; :: thesis: (All z,F) . a = ((All s,H) / x,y) . a
then A10: ( ( a = 1 or a = 2 ) & x <> 4 & a in dom <*4,z*> ) by A3, Th148, TARSKI:def 2;
( (All z,F) . a1 = <*4,z*> . a1 & (All s,H) . a1 = <*4,s*> . a1 & <*4,z*> . 1 = 4 & <*4,s*> . 1 = 4 & <*4,z*> . 2 = z & <*4,s*> . 2 = s ) by A3, A9, FINSEQ_1:61, FINSEQ_1:def 7;
hence (All z,F) . a = ((All s,H) / x,y) . a by A4, A6, A7, A10, Def4; :: thesis: verum

end;

now

given i being Nat such that A11: ( i in dom H & a1 = 2 + i ) ; :: thesis: (All z,F) . a = ((All s,H) / x,y) . a
( (All z,F) . a = F . i & (All s,H) . a = H . i ) by A1, A5, A11, FINSEQ_1:def 7;
then ( ( (All s,H) . a <> x implies (All z,F) . a = (All s,H) . a ) & ( (All s,H) . a = x implies (All z,F) . a = y ) & ( (All s,H) . a <> x implies ((All s,H) / x,y) . a = (All s,H) . a ) & ( (All s,H) . a = x implies ((All s,H) / x,y) . a = y ) ) by A4, A6, A7, A11, Def4;
hence (All z,F) . a = ((All s,H) / x,y) . a ; :: thesis: verum

end;

hence (All z,F) . a = ((All s,H) / x,y) . a by A1, A3, A6, A7, A8, FINSEQ_1:38; :: thesis: verum

end;

hence All z,F = (All s,H) / x,y by A6, FUNCT_1:9; :: thesis: verum