let A be non empty set ; :: thesis:
let J be interpretation of A; :: thesis:
let v be Element of Valuations_in A; :: thesis:
let f be FinSequence of CQC-WFF ; :: thesis:
assume A1: len f > 0 ; :: thesis:
thus ( J,v |= Ant f & J,v |= Suc f implies J,v |= f ) :: thesis:

assume that
A2: J,v |= Ant f and
A3: J,v |= Suc f ; :: thesis:
let p be Element of CQC-WFF ; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis:
assume p in rng f ; :: thesis:
then p in (rng (Ant f)) \/ {(Suc f)} by A1, Th3;
then A4: ( p in rng (Ant f) or p in {(Suc f)} ) by XBOOLE_0:def 3;
J,v |= rng (Ant f) by A2, Def14;
hence J,v |= p by A3, A4, Def11, TARSKI:def 1; :: thesis:

end;

thus ( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) ) :: thesis:

assume A5: J,v |= rng f ; :: according to CALCUL_1:def 14 :: thesis:
thus J,v |= rng (Ant f) :: according to CALCUL_1:def 14 :: thesis:

A6: rng (Ant f) c= (rng (Ant f)) \/ {(Suc f)} by XBOOLE_1:7;
let p be Element of CQC-WFF ; :: according to CALCUL_1:def 11 :: thesis:
assume p in rng (Ant f) ; :: thesis:
then p in (rng (Ant f)) \/ {(Suc f)} by A6;
then p in rng f by A1, Th3;
hence J,v |= p by A5, Def11; :: thesis:

end;

0 + 1 <= len f by A1, NAT_1:13;
then A7: len f in dom f by FINSEQ_3:27;
Suc f = f . (len f) by A1, Def2;
then Suc f in rng f by A7, FUNCT_1:12;
hence J,v |= Suc f by A5, Def11; :: thesis:

end;