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

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