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

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