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