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