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