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