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;
A4: now :: thesis: for j being Nat st j in dom f holds
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;
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;
A9: now :: thesis: ( j = (len (Ant f)) + 1 implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )
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;
j <= (len (Ant f)) + 1 by A2, A3, A5, FINSEQ_1:1;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A7, A9, NAT_1:8; :: thesis: verum
end;
len f = (len (Ant f)) + (len <*(Suc f)*>) by A2, FINSEQ_1:39;
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