let H, G, H1, G1 be LTL-formula; :: thesis: ( H '&' G = H1 '&' G1 implies ( H = H1 & G = G1 ) )
assume A1: H '&' G = H1 '&' G1 ; :: thesis: ( H = H1 & G = G1 )
( H '&' G = (<*1*> ^ H) ^ G & H1 '&' G1 = (<*1*> ^ H1) ^ G1 & (<*1*> ^ H) ^ G = <*1*> ^ (H ^ G) & (<*1*> ^ H1) ^ G1 = <*1*> ^ (H1 ^ G1) ) by FINSEQ_1:45;
then H ^ G = H1 ^ G1 by A1, FINSEQ_1:46;
then A2: ( ( len H <= len H1 or len H1 <= len H ) & ( len H1 <= len H implies ex sq being FinSequence st H = H1 ^ sq ) & ( len H <= len H1 implies ex sq being FinSequence st H1 = H ^ sq ) ) by FINSEQ_1:64;
A3: ( ex sq being FinSequence st H1 = H ^ sq implies H1 = H ) by Lm11;
thus H = H1 by A2, Lm11; :: thesis: G = G1
thus G = G1 by A1, A2, A3, Lm11, FINSEQ_1:46; :: thesis: verum