let F, H be ZF-formula; 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; ( 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 ) )
; 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 for a being object st a in dom ((All (s,H)) / (x,y)) holds
(All (z,F)) . a = ((All (s,H)) / (x,y)) . alet a be
object ;
( 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))
;
(All (z,F)) . a = ((All (s,H)) / (x,y)) . athen reconsider a1 =
a as
Element of
NAT by A6;
A14:
now ( a in {1,2} implies (All (z,F)) . a = ((All (s,H)) / (x,y)) . a )A15:
(
x <> 4 &
<*4,z*> . 1
= 4 )
by Th135, FINSEQ_1:44;
A16:
(
<*4,s*> . 1
= 4 &
<*4,z*> . 2
= z )
by FINSEQ_1:44;
A17:
<*4,s*> . 2
= s
by FINSEQ_1:44;
assume A18:
a in {1,2}
;
(All (z,F)) . a = ((All (s,H)) / (x,y)) . athen 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, Def3;
verum end; now ( 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
;
(All (z,F)) . a = ((All (s,H)) / (x,y)) . aA23:
(
(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;
verum end; hence
(All (z,F)) . a = ((All (s,H)) / (x,y)) . a
by A2, A3, A6, A13, A14, FINSEQ_1:25;
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; verum