let G, G1, H, H1 be CTL-formula; :: thesis: ( H '&' G = H1 '&' G1 implies ( H = H1 & G = G1 ) )
assume A1: H '&' G = H1 '&' G1 ; :: thesis: ( H = H1 & G = G1 )
A2: (<*1*> ^ H1) ^ G1 = <*1*> ^ (H1 ^ G1) by FINSEQ_1:32;
(<*1*> ^ H) ^ G = <*1*> ^ (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