:: deftheorem defines * PRELAMB:def 3 :
for s being non empty typealg
for x, y being type of s holds x * y = the inner_product of s . (x,y);