let p be Element of CQC-WFF ; :: thesis: for f, g being FinSequence of CQC-WFF st |- f ^ <*p*> holds
|- (f ^ g) ^ <*p*>
let f, g be FinSequence of CQC-WFF ; :: thesis: ( |- f ^ <*p*> implies |- (f ^ g) ^ <*p*> )
assume A1: |- f ^ <*p*> ; :: thesis: |- (f ^ g) ^ <*p*>
A2: ( Ant (f ^ <*p*>) = f & Ant ((f ^ g) ^ <*p*>) = f ^ g & Suc ((f ^ g) ^ <*p*>) = p ) by CALCUL_1:5;
then Suc (f ^ <*p*>) = Suc ((f ^ g) ^ <*p*>) by CALCUL_1:5;
hence |- (f ^ g) ^ <*p*> by A1, A2, CALCUL_1:8, CALCUL_1:36; :: thesis: verum