let H, G, H1, G1 be LTL-formula; :: thesis: ( H 'or' G = H1 'or' G1 implies ( H = H1 & G = G1 ) )
assume A1: H 'or' G = H1 'or' G1 ; :: thesis: ( H = H1 & G = G1 )
( H 'or' G = (<*2*> ^ H) ^ G & H1 'or' G1 = (<*2*> ^ H1) ^ G1 & (<*2*> ^ H) ^ G = <*2*> ^ (H ^ G) & (<*2*> ^ H1) ^ G1 = <*2*> ^ (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