let G, G1, H, H1 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 )
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; :: thesis: 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; :: thesis: verum