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