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

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