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