let G, G1, H, H1 be LTL-formula; :: thesis: ( H 'R' G = H1 'R' G1 implies ( H = H1 & G = G1 ) )
assume A1: H 'R' G = H1 'R' G1 ; :: thesis: ( H = H1 & G = G1 )
( (<*5*> ^ H) ^ G = <*5*> ^ (H ^ G) & (<*5*> ^ H1) ^ G1 = <*5*> ^ (H1 ^ G1) ) by FINSEQ_1:32;
then A2: H ^ G = H1 ^ G1 by A1, FINSEQ_1:33;
then A3: ( len H1 <= len H implies ex sq being FinSequence st H = H1 ^ sq ) by FINSEQ_1:47;
A4: ( len H <= len H1 implies ex sq being FinSequence st H1 = H ^ sq ) by A2, FINSEQ_1:47;
hence H = H1 by A3, Lm11; :: thesis: G = G1
( ex sq being FinSequence st H1 = H ^ sq implies H1 = H ) by Lm11;
hence G = G1 by A1, A3, A4, Lm11, FINSEQ_1:33; :: thesis: verum