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