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