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