let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds

( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) )

assume A1: len f > 0 ; :: thesis: ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

then A2: len f = (len (Ant f)) + 1 by Th2;

A3: dom f = Seg (len f) by FINSEQ_1:def 3;

then A12: len f = len ((Ant f) ^ <*(Suc f)*>) by FINSEQ_1:22;

then f = (Ant f) ^ <*(Suc f)*> by A4, FINSEQ_2:9;

then rng f = (rng (Ant f)) \/ (rng <*(Suc f)*>) by FINSEQ_1:31;

hence ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) by A12, A4, FINSEQ_1:38, FINSEQ_2:9; :: thesis: verum

( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) )

assume A1: len f > 0 ; :: thesis: ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

then A2: len f = (len (Ant f)) + 1 by Th2;

A3: dom f = Seg (len f) by FINSEQ_1:def 3;

A4: now :: thesis: for j being Nat st j in dom f holds

f . j = ((Ant f) ^ <*(Suc f)*>) . j

len f = (len (Ant f)) + (len <*(Suc f)*>)
by A2, FINSEQ_1:39;f . j = ((Ant f) ^ <*(Suc f)*>) . j

let j be Nat; :: thesis: ( j in dom f implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )

assume A5: j in dom f ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j

A6: 1 <= j by A3, A5, FINSEQ_1:1;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A7, A9, NAT_1:8; :: thesis: verum

end;assume A5: j in dom f ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j

A6: 1 <= j by A3, A5, FINSEQ_1:1;

A7: now :: thesis: ( j <= len (Ant f) implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )

assume
j <= len (Ant f)
; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j

then A8: j in dom (Ant f) by A6, FINSEQ_3:25;

Ant f = f | (Seg (len (Ant f))) by A2, Def1;

then Ant f = f | (dom (Ant f)) by FINSEQ_1:def 3;

then f . j = (Ant f) . j by A8, FUNCT_1:49;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A8, FINSEQ_1:def 7; :: thesis: verum

end;then A8: j in dom (Ant f) by A6, FINSEQ_3:25;

Ant f = f | (Seg (len (Ant f))) by A2, Def1;

then Ant f = f | (dom (Ant f)) by FINSEQ_1:def 3;

then f . j = (Ant f) . j by A8, FUNCT_1:49;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A8, FINSEQ_1:def 7; :: thesis: verum

A9: now :: thesis: ( j = (len (Ant f)) + 1 implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )

j <= (len (Ant f)) + 1
by A2, A3, A5, FINSEQ_1:1;
1 in Seg 1
by FINSEQ_1:1;

then A10: 1 in dom <*(Suc f)*> by FINSEQ_1:38;

assume A11: j = (len (Ant f)) + 1 ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j

then j = len f by A1, Th2;

then f . j = Suc f by A1, Def2;

then f . j = <*(Suc f)*> . 1 by FINSEQ_1:40;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A11, A10, FINSEQ_1:def 7; :: thesis: verum

end;then A10: 1 in dom <*(Suc f)*> by FINSEQ_1:38;

assume A11: j = (len (Ant f)) + 1 ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j

then j = len f by A1, Th2;

then f . j = Suc f by A1, Def2;

then f . j = <*(Suc f)*> . 1 by FINSEQ_1:40;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A11, A10, FINSEQ_1:def 7; :: thesis: verum

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A7, A9, NAT_1:8; :: thesis: verum

then A12: len f = len ((Ant f) ^ <*(Suc f)*>) by FINSEQ_1:22;

then f = (Ant f) ^ <*(Suc f)*> by A4, FINSEQ_2:9;

then rng f = (rng (Ant f)) \/ (rng <*(Suc f)*>) by FINSEQ_1:31;

hence ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) by A12, A4, FINSEQ_1:38, FINSEQ_2:9; :: thesis: verum