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:56;
len <*s*> = 1 by FINSEQ_1:56;
then A2: len (<*4*> ^ <*s*>) = 2 by A1, FINSEQ_1:35;
then A3: dom (<*4*> ^ <*s*>) = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
len (All s,H) = 2 + (len H) by A2, FINSEQ_1:35;
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 Def4;
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, Def4;
len <*z*> = 1 by FINSEQ_1:56;
then A10: len (<*4*> ^ <*z*>) = 2 by A1, FINSEQ_1:35;
then A11: dom (<*4*> ^ <*z*>) = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;

A12: 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 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

A15: ( x <> 4 & <*4,z*> . 1 = 4 ) by Th148, FINSEQ_1:61;
A16: ( <*4,s*> . 1 = 4 & <*4,z*> . 2 = z ) by FINSEQ_1:61;
A17: <*4,s*> . 2 = s by FINSEQ_1:61;
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, A16, A17, Def4; :: thesis: verum

end;

now

A20: ( (All s,H) . a <> x implies ((All s,H) / x,y) . a = (All s,H) . a ) by A6, A13, Def4;
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, Def4;
( (All s,H) . a <> x implies (All z,F) . a = (All s,H) . a ) by A7, A21, A23, Def4;
hence (All z,F) . a = ((All s,H) / x,y) . a by A6, A13, A24, A20, Def4; :: thesis: verum

end;

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

end;

len (All z,F) = 2 + (len F) by A10, FINSEQ_1:35;
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:31;
hence All z,F = (All s,H) / x,y by A6, A12, FUNCT_1:9; :: thesis: verum