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