let S1, S2 be Element of QC-Sub-WFF A; :: thesis: ( ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S1,S9) & S1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st
( S = Sub_& (S2,S9) & S2 `2 = S9 `2 ) implies S1 = S2 )
given T1 being Element of QC-Sub-WFF A such that A1: ( S = Sub_& (S1,T1) & S1 `2 = T1 `2 ) ; :: thesis: ( for S9 being Element of QC-Sub-WFF A holds
( not S = Sub_& (S2,S9) or not S2 `2 = S9 `2 ) or S1 = S2 )
given T2 being Element of QC-Sub-WFF A such that A2: ( S = Sub_& (S2,T2) & S2 `2 = T2 `2 ) ; :: thesis: S1 = S2
A3: ( len (@ (S1 `1)) <= len (@ (S2 `1)) or len (@ (S2 `1)) <= len (@ (S1 `1)) ) ;
A4: S = [((S2 `1) '&' (T2 `1)),(S2 `2)] by A2, Def21;
A5: S = [((S1 `1) '&' (T1 `1)),(S1 `2)] by A1, Def21;
then (S1 `1) '&' (T1 `1) = (S2 `1) '&' (T2 `1) by A4, 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 (@ (S1 `1)) ^ (@ (T1 `1)) = (@ (S2 `1)) ^ (@ (T2 `1)) by FINSEQ_1:33;
then consider a, b, c, d being FinSequence such that
A6: ( ( a = @ (S1 `1) & b = @ (S2 `1) ) or ( a = @ (S2 `1) & b = @ (S1 `1) ) ) and
A7: ( len a <= len b & a ^ c = b ^ d ) by A3;
A8: ( S1 = [(S1 `1),(S1 `2)] & S2 = [(S2 `1),(S2 `2)] ) by Th10;
ex t being FinSequence st a ^ t = b by A7, FINSEQ_1:47;
then S1 `1 = S2 `1 by A6, QC_LANG1:13;
hence S1 = S2 by A5, A4, A8, XTUPLE_0:1; :: thesis: verum