let T1, T2 be Element of QC-Sub-WFF ; :: thesis: ( ex S9 being Element of QC-Sub-WFF st
( S = Sub_& S9,T1 & S9 `2 = T1 `2 ) & ex S9 being Element of QC-Sub-WFF st
( S = Sub_& S9,T2 & S9 `2 = T2 `2 ) implies T1 = T2 )
given S1 being Element of QC-Sub-WFF such that A3: ( S = Sub_& S1,T1 & S1 `2 = T1 `2 ) ; :: thesis: ( for S9 being Element of QC-Sub-WFF holds
( not S = Sub_& S9,T2 or not S9 `2 = T2 `2 ) or T1 = T2 )
A4: ( T1 = [(T1 `1 ),(T1 `2 )] & T2 = [(T2 `1 ),(T2 `2 )] ) by Th10;
given S2 being Element of QC-Sub-WFF such that A5: ( S = Sub_& S2,T2 & S2 `2 = T2 `2 ) ; :: thesis: T1 = T2
A6: S = [((S1 `1 ) '&' (T1 `1 )),(T1 `2 )] by A3, Def21;
A7: S = [((S2 `1 ) '&' (T2 `1 )),(T2 `2 )] by A5, Def21;
then (S1 `1 ) '&' (T1 `1 ) = (S2 `1 ) '&' (T2 `1 ) by A6, ZFMISC_1:33;
then <*[2,0 ]*> ^ ((@ (S1 `1 )) ^ (@ (T1 `1 ))) = (S2 `1 ) '&' (T2 `1 ) by FINSEQ_1:45
.= <*[2,0 ]*> ^ ((@ (S2 `1 )) ^ (@ (T2 `1 ))) by FINSEQ_1:45 ;
then A8: (@ (S1 `1 )) ^ (@ (T1 `1 )) = (@ (S2 `1 )) ^ (@ (T2 `1 )) by FINSEQ_1:46;
S1 = Sub_the_left_argument_of S by A1, A3, Def31
.= S2 by A1, A5, Def31 ;
then @ (T1 `1 ) = @ (T2 `1 ) by A8, FINSEQ_1:46;
hence T1 = T2 by A6, A7, A4, ZFMISC_1:33; :: thesis: verum