let I be non empty set ; :: thesis: for F being Group-Family of I
for a, b being Element of (product F)
for i being Element of I holds [.a,b.] . i = [.(a /. i),(b /. i).]
let F be Group-Family of I; :: thesis: for a, b being Element of (product F)
for i being Element of I holds [.a,b.] . i = [.(a /. i),(b /. i).]
let a, b be Element of (product F); :: thesis: for i being Element of I holds [.a,b.] . i = [.(a /. i),(b /. i).]
let i be Element of I; :: thesis: [.a,b.] . i = [.(a /. i),(b /. i).]
thus [.(a /. i),(b /. i).] = (((a /. i) ") * ((b /. i) ")) * ((a /. i) * (b /. i)) by GROUP_5:16
.= (((a ") /. i) * ((b /. i) ")) * ((a /. i) * (b /. i)) by GROUP_7:8
.= (((a ") /. i) * ((b ") /. i)) * ((a /. i) * (b /. i)) by GROUP_7:8
.= (((a ") /. i) * ((b ") /. i)) * ((a * b) /. i) by GROUP_7:1
.= (((a ") * (b ")) /. i) * ((a * b) /. i) by GROUP_7:1
.= (((a ") * (b ")) * (a * b)) /. i by GROUP_7:1
.= [.a,b.] . i by GROUP_5:16 ; :: thesis: verum