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

( (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