let K be Field; :: thesis: for a, b being Element of K holds the multF of K $$ <*a,b*> = a * b
let a, b be Element of K; :: thesis: the multF of K $$ <*a,b*> = a * b
the multF of K $$ <*a,b*> = Product <*a,b*> by GROUP_4:def 2
.= a * b by GROUP_4:10 ;
hence the multF of K $$ <*a,b*> = a * b ; :: thesis: verum