let G be Group; :: thesis: for a, b, c being Element of G holds <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
let a, b, c be Element of G; :: thesis: <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
thus <*a,b*> |^ c = (<*a*> ^ <*b*>) |^ c by FINSEQ_1:def 9
.= (<*a*> |^ c) ^ (<*b*> |^ c) by Th9
.= <*(a |^ c)*> ^ (<*b*> |^ c) by Th11
.= <*(a |^ c)*> ^ <*(b |^ c)*> by Th11
.= <*(a |^ c),(b |^ c)*> by FINSEQ_1:def 9 ; :: thesis: verum