let p, q be Element of CQC-WFF ; :: thesis: ( ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = q & S `2 = Sub ) ) implies for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p '&' q & S `2 = Sub ) )
assume A1: ( ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = q & S `2 = Sub ) ) ) ; :: thesis: for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = p '&' q & S `2 = Sub )
let Sub be CQC_Substitution; :: thesis: ex S being Element of CQC-Sub-WFF st
( S `1 = p '&' q & S `2 = Sub )
consider S1 being Element of CQC-Sub-WFF such that
A2: ( S1 `1 = p & S1 `2 = Sub ) by A1;
consider S2 being Element of CQC-Sub-WFF such that
A3: ( S2 `1 = q & S2 `2 = Sub ) by A1;
( S1 = [p,Sub] & S2 = [q,Sub] ) by A2, A3, SUBSTUT1:10;
then ( [p,Sub] in QC-Sub-WFF & [q,Sub] in QC-Sub-WFF ) ;
then ( [(@ p),Sub] in QC-Sub-WFF & [(@ q),Sub] in QC-Sub-WFF ) by QC_LANG1:def 12;
then [((<*[2,0 ]*> ^ (@ p)) ^ (@ q)),Sub] in QC-Sub-WFF by SUBSTUT1:def 16;
then reconsider S = [(p '&' q),Sub] as Element of QC-Sub-WFF by QC_LANG1:def 15;
take S ; :: thesis: ( S is Element of CQC-Sub-WFF & S `1 = p '&' q & S `2 = Sub )
S `1 = p '&' q by MCART_1:7;
then S in CQC-Sub-WFF by SUBSTUT1:def 39;
then reconsider S = S as Element of CQC-Sub-WFF ;
S `2 = Sub by MCART_1:7;
hence ( S is Element of CQC-Sub-WFF & S `1 = p '&' q & S `2 = Sub ) by MCART_1:7; :: thesis: verum