let A be QC-alphabet ; :: thesis: for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds
( S1 = S19 & S2 = S29 )
let S1, S2, S19, S29 be Element of QC-Sub-WFF A; :: 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 XTUPLE_0:1;
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:2; :: thesis: verum