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