let S1, S2, S1', S2' be Element of QC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 & S1' `2 = S2' `2 & Sub_& S1,S2 = Sub_& S1',S2' implies ( S1 = S1' & S2 = S2' ) )
assume that
A1: S1 `2 = S2 `2 and
A2: S1' `2 = S2' `2 and
A3: Sub_& S1,S2 = Sub_& S1',S2' ; :: thesis: ( S1 = S1' & S2 = S2' )
Sub_& S1,S2 = [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )] by A1, Def21;
then [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )] = [((S1' `1 ) '&' (S2' `1 )),(S1' `2 )] by A2, A3, Def21;
then A4: ( (S1 `1 ) '&' (S2 `1 ) = (S1' `1 ) '&' (S2' `1 ) & S1 `2 = S1' `2 ) by ZFMISC_1:33;
A5: ( S2 = [(S2 `1 ),(S2 `2 )] & S2' = [(S2' `1 ),(S2' `2 )] ) by Th10;
( S1 = [(S1 `1 ),(S1 `2 )] & S1' = [(S1' `1 ),(S1' `2 )] ) by Th10;
hence ( S1 = S1' & S2 = S2' ) by A1, A2, A4, A5, QC_LANG2:3; :: thesis: verum