let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds
( (len (Ant f)) + 1 = len f & len (Ant f) < len f )
let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( (len (Ant f)) + 1 = len f & len (Ant f) < len f ) )
assume len f > 0 ; :: thesis: ( (len (Ant f)) + 1 = len f & len (Ant f) < len f )
then consider i being Nat such that
A1: len f = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
Ant f = f | (Seg i) by A1, Def1;
then dom (Ant f) = (dom f) /\ (Seg i) by RELAT_1:61;
then Seg (len (Ant f)) = (dom f) /\ (Seg i) by FINSEQ_1:def 3;
then A2: Seg (len (Ant f)) = (Seg (len f)) /\ (Seg i) by FINSEQ_1:def 3;
i <= len f by A1, NAT_1:11;
then A3: Seg i c= Seg (len f) by FINSEQ_1:5;
hence (len (Ant f)) + 1 = len f by A1, A2, FINSEQ_1:6, XBOOLE_1:28; :: thesis: len (Ant f) < len f
len (Ant f) = i by A2, A3, FINSEQ_1:6, XBOOLE_1:28;
hence len (Ant f) < len f by A1, NAT_1:13; :: thesis: verum