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