let H, F 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 )
A1: 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 A2: 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 A3: ( len H = n & H = F ^ sq ) ; :: thesis: H = F
A4: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:35;
A5: dom F = Seg (len F) by FINSEQ_1:def 3;
( 1 <= 3 & 3 <= len F ) by Th29;
then ( 1 <= 1 & 1 <= len F ) by XXREAL_0:2;
then A6: 1 in dom F by A5, FINSEQ_1:3;

A7: now

assume H is atomic ; :: thesis: H = F
then A8: len H = 3 by Th27;
then ( len F <= 3 & 3 <= len F ) by A3, A4, Th29, NAT_1:11;
then 3 + (len sq) = 3 + 0 by A3, A4, A8, XXREAL_0:1;
then sq = {} ;
hence H = F by A3, FINSEQ_1:47; :: thesis: verum

end;

A9: now

assume A10: H is negative ; :: thesis: H = F
then consider H1 being ZF-formula such that
A11: H = 'not' H1 by Def12;
(F ^ sq) . 1 = 2 by A3, A10, Th37;
then F . 1 = 2 by A6, FINSEQ_1:def 7;
then F is negative by Th40;
then consider F1 being ZF-formula such that
A12: F = 'not' F1 by Def12;
( 'not' H1 = <*2*> ^ H1 & 'not' F1 = <*2*> ^ F1 & (<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) ) by FINSEQ_1:45;
then A13: H1 = F1 ^ sq by A3, A11, A12, FINSEQ_1:46;
( (len <*2*>) + (len H1) = len H & (len H1) + 1 = 1 + (len H1) & len <*2*> = 1 ) by A11, FINSEQ_1:35, FINSEQ_1:57;
then len H1 < len H by NAT_1:13;
hence H = F by A2, A3, A11, A12, A13; :: thesis: verum

end;

A14: now

assume A15: H is universal ; :: thesis: H = F
then consider x being Variable, H1 being ZF-formula such that
A16: H = All x,H1 by Def14;
(F ^ sq) . 1 = 4 by A3, A15, Th39;
then F . 1 = 4 by A6, FINSEQ_1:def 7;
then F is universal by Th40;
then consider y being Variable, F1 being ZF-formula such that
A17: F = All y,F1 by Def14;
A18: ( All x,H1 = (<*4*> ^ <*x*>) ^ H1 & All y,F1 = (<*4*> ^ <*y*>) ^ F1 & ((<*4*> ^ <*y*>) ^ F1) ^ sq = (<*4*> ^ <*y*>) ^ (F1 ^ sq) & (<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) & (<*4*> ^ <*y*>) ^ (F1 ^ sq) = <*4*> ^ (<*y*> ^ (F1 ^ sq)) ) by FINSEQ_1:45;
then A19: <*x*> ^ H1 = <*y*> ^ (F1 ^ sq) by A3, A16, A17, FINSEQ_1:46;
( (<*x*> ^ H1) . 1 = x & (<*y*> ^ (F1 ^ sq)) . 1 = y ) by FINSEQ_1:58;
then A20: H1 = F1 ^ sq by A19, FINSEQ_1:46;
( (len (<*4*> ^ <*x*>)) + (len H1) = len H & len <*4,x*> = 2 & (len H1) + 1 = 1 + (len H1) & 1 + (1 + (len H1)) = (1 + (len H1)) + 1 & (1 + 1) + (len H1) = 1 + (1 + (len H1)) & <*4*> ^ <*x*> = <*4,x*> ) by A16, FINSEQ_1:35, FINSEQ_1:61, FINSEQ_1:def 9;
then (len H1) + 1 <= len H by NAT_1:11;
then len H1 < len H by NAT_1:13;
hence H = F by A2, A3, A17, A18, A20; :: thesis: verum

end;

now

assume A21: H is conjunctive ; :: thesis: H = F
then consider G1, G being ZF-formula such that
A22: H = G1 '&' G by Def13;
( (F ^ sq) . 1 = 3 & 1 <= 1 ) by A3, A21, Th38;
then F . 1 = 3 by A6, FINSEQ_1:def 7;
then F is conjunctive by Th40;
then consider F1, H1 being ZF-formula such that
A23: F = F1 '&' H1 by Def13;
( G1 '&' G = (<*3*> ^ G1) ^ G & F1 '&' H1 = (<*3*> ^ F1) ^ H1 & (<*3*> ^ G1) ^ G = <*3*> ^ (G1 ^ G) & (<*3*> ^ F1) ^ H1 = <*3*> ^ (F1 ^ H1) & (<*3*> ^ (F1 ^ H1)) ^ sq = <*3*> ^ ((F1 ^ H1) ^ sq) & (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) ) by FINSEQ_1:45;
then A24: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A22, A23, FINSEQ_1:46;
then A25: ( ( len G1 <= len F1 or len F1 <= len G1 ) & ( len F1 <= len G1 implies ex sq' being FinSequence st G1 = F1 ^ sq' ) & ( len G1 <= len F1 implies ex sq' being FinSequence st F1 = G1 ^ sq' ) ) by FINSEQ_1:64;

A26: now

given sq' being FinSequence such that A27: G1 = F1 ^ sq' ; :: thesis: G1 = F1
( (len (<*3*> ^ G1)) + (len G) = len H & len (<*3*> ^ G1) = (len <*3*>) + (len G1) & len <*3*> = 1 & 1 + (len G1) = (len G1) + 1 ) by A22, FINSEQ_1:35, FINSEQ_1:57;
then (len G1) + 1 <= len H by NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A2, A3, A27; :: thesis: verum

end;

A28: now

given sq' being FinSequence such that A29: F1 = G1 ^ sq' ; :: thesis: F1 = G1
( len (F ^ sq) = (len F) + (len sq) & len <*3*> = 1 & len (<*3*> ^ F1) = (len <*3*>) + (len F1) & 1 + (len F1) = (len F1) + 1 & len F = (len (<*3*> ^ F1)) + (len H1) & len <*3*> = 1 & (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ) by A23, FINSEQ_1:35, FINSEQ_1:57;
then (len F1) + 1 <= len H by A3, NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A2, A3, A29; :: thesis: verum

end;

then A30: G = H1 ^ sq by A24, A25, A26, FINSEQ_1:46;
( (len (<*3*> ^ G1)) + (len G) = len H & len (<*3*> ^ G1) = (len <*3*>) + (len G1) & len <*3*> = 1 & (1 + (len G1)) + (len G) = (len G) + (1 + (len G1)) & (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ) by A22, FINSEQ_1:35, FINSEQ_1:57;
then (len G) + 1 <= len H by NAT_1:11;
then len G < len H by NAT_1:13;
hence H = F by A2, A3, A22, A23, A25, A26, A28, A30; :: thesis: verum

end;

hence H = F by A7, A9, A14, Th26; :: thesis: verum

end;

defpred S₁[ Nat] means for H, F being ZF-formula
for sq being FinSequence st len H = $1 & H = F ^ sq holds
H = F;
A31: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k] by A1;
A32: for n being Nat holds S₁[n] from NAT_1:sch 4(A31);
len H = len H ;
hence ( H = F ^ sq implies H = F ) by A32; :: thesis: verum