let G, G1, H, H1 be LTL-formula; ( H 'R' G = H1 'R' G1 implies ( H = H1 & G = G1 ) )
assume A1:
H 'R' G = H1 'R' G1
; ( 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; 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; verum