let F, H be ZF-formula; :: thesis: for sq being FinSequence st H = F ^ sq holds
H = F
let sq be FinSequence; :: thesis: ( H = F ^ sq implies H = F )
defpred S₁[ Nat] means for H, F being ZF-formula
for sq being FinSequence st len H = $1 & H = F ^ sq holds
H = F;
for n being Nat st ( for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) holds
for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) implies for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F )
assume A1: for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ; :: thesis: for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let H, F be ZF-formula; :: thesis: for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let sq be FinSequence; :: thesis: ( len H = n & H = F ^ sq implies H = F )
assume that
A2: len H = n and
A3: H = F ^ sq ; :: thesis: H = F
3 <= len F by Th13;
then ( dom F = Seg (len F) & 1 <= len F ) by FINSEQ_1:def 3, XXREAL_0:2;
then A4: 1 in dom F by FINSEQ_1:1;

A5: now :: thesis: ( H is negative implies H = F )

A6: len <*2*> = 1 by FINSEQ_1:40;
assume A7: H is negative ; :: thesis: H = F
then consider H1 being ZF-formula such that
A8: H = 'not' H1 ;
(F ^ sq) . 1 = 2 by A3, A7, Th20;
then F . 1 = 2 by A4, FINSEQ_1:def 7;
then F is negative by Th23;
then consider F1 being ZF-formula such that
A9: F = 'not' F1 ;
(len <*2*>) + (len H1) = len H by A8, FINSEQ_1:22;
then A10: len H1 < len H by A6, NAT_1:13;
(<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) by FINSEQ_1:32;
then H1 = F1 ^ sq by A3, A8, A9, FINSEQ_1:33;
hence H = F by A1, A2, A8, A9, A10; :: thesis: verum

end;

A11: now :: thesis: ( H is conjunctive implies H = F )

assume A12: H is conjunctive ; :: thesis: H = F
then consider G1, G being ZF-formula such that
A13: H = G1 '&' G ;
A14: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ;
A15: ( len (<*3*> ^ G1) = (len <*3*>) + (len G1) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
(len (<*3*> ^ G1)) + (len G) = len H by A13, FINSEQ_1:22;
then (len G) + 1 <= len H by A15, A14, NAT_1:11;
then A16: len G < len H by NAT_1:13;
(F ^ sq) . 1 = 3 by A3, A12, Th21;
then F . 1 = 3 by A4, FINSEQ_1:def 7;
then F is conjunctive by Th23;
then consider F1, H1 being ZF-formula such that
A17: F = F1 '&' H1 ;

A18: now :: thesis: ( ex sq9 being FinSequence st F1 = G1 ^ sq9 implies F1 = G1 )

A19: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A20: F1 = G1 ^ sq9 ; :: thesis: F1 = G1
A21: ( len (F ^ sq) = (len F) + (len sq) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
( len (<*3*> ^ F1) = (len <*3*>) + (len F1) & len F = (len (<*3*> ^ F1)) + (len H1) ) by A17, FINSEQ_1:22;
then (len F1) + 1 <= len H by A3, A21, A19, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1, A2, A20; :: thesis: verum

end;

A22: ( (<*3*> ^ F1) ^ H1 = <*3*> ^ (F1 ^ H1) & (<*3*> ^ (F1 ^ H1)) ^ sq = <*3*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;

A23: now :: thesis: ( ex sq9 being FinSequence st G1 = F1 ^ sq9 implies G1 = F1 )

given sq9 being FinSequence such that A24: G1 = F1 ^ sq9 ; :: thesis: G1 = F1
A25: len <*3*> = 1 by FINSEQ_1:40;
( (len (<*3*> ^ G1)) + (len G) = len H & len (<*3*> ^ G1) = (len <*3*>) + (len G1) ) by A13, FINSEQ_1:22;
then (len G1) + 1 <= len H by A25, NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1, A2, A24; :: thesis: verum

end;

A26: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32;
(<*3*> ^ G1) ^ G = <*3*> ^ (G1 ^ G) by FINSEQ_1:32;
then A27: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A13, A17, A22, A26, FINSEQ_1:33;
then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A27, A23, A18, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A17, A22, A26, A16; :: thesis: verum

end;

A28: now :: thesis: ( H is universal implies H = F )

assume A29: H is universal ; :: thesis: H = F
then consider x being Variable, H1 being ZF-formula such that
A30: H = All (x,H1) ;
A31: <*4*> ^ <*x*> = <*4,x*> by FINSEQ_1:def 9;
A32: ( len <*4,x*> = 2 & 1 + (1 + (len H1)) = (1 + (len H1)) + 1 ) by FINSEQ_1:44;
(len (<*4*> ^ <*x*>)) + (len H1) = len H by A30, FINSEQ_1:22;
then (len H1) + 1 <= len H by A32, A31, NAT_1:11;
then A33: len H1 < len H by NAT_1:13;
(F ^ sq) . 1 = 4 by A3, A29, Th22;
then F . 1 = 4 by A4, FINSEQ_1:def 7;
then F is universal by Th23;
then consider y being Variable, F1 being ZF-formula such that
A34: F = All (y,F1) ;
A35: ( (<*x*> ^ H1) . 1 = x & (<*y*> ^ (F1 ^ sq)) . 1 = y ) by FINSEQ_1:41;
A36: ((<*4*> ^ <*y*>) ^ F1) ^ sq = (<*4*> ^ <*y*>) ^ (F1 ^ sq) by FINSEQ_1:32;
( (<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) & (<*4*> ^ <*y*>) ^ (F1 ^ sq) = <*4*> ^ (<*y*> ^ (F1 ^ sq)) ) by FINSEQ_1:32;
then <*x*> ^ H1 = <*y*> ^ (F1 ^ sq) by A3, A30, A34, A36, FINSEQ_1:33;
then H1 = F1 ^ sq by A35, FINSEQ_1:33;
hence H = F by A1, A2, A3, A34, A36, A33; :: thesis: verum

end;

A37: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:22;

now :: thesis: ( H is atomic implies H = F )

A38: 3 <= len F by Th13;
assume H is atomic ; :: thesis: H = F
then A39: len H = 3 by Th11;
then len F <= 3 by A3, A37, NAT_1:11;
then 3 + (len sq) = 3 + 0 by A3, A37, A39, A38, XXREAL_0:1;
then sq = {} ;
hence H = F by A3, FINSEQ_1:34; :: thesis: verum

end;

hence H = F by A5, A28, A11, Th10; :: thesis: verum

end;

then A40: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k] ;
A41: for n being Nat holds S₁[n] from NAT_1:sch 4(A40);
len H = len H ;
hence ( H = F ^ sq implies H = F ) by A41; :: thesis: verum