let x, y be PartFunc of REAL,REAL; :: thesis: for t being Real holds (x (#) y) . t <= (1 / 2) * (((x (#) x) . t) + ((y (#) y) . t))
let t be Real; :: thesis: (x (#) y) . t <= (1 / 2) * (((x (#) x) . t) + ((y (#) y) . t))
A1: (x (#) y) . t = (x . t) * (y . t) by VALUED_1:5;
((x (#) x) . t) + ((y (#) y) . t) = ((x . t) * (x . t)) + ((y (#) y) . t) by VALUED_1:5
.= ((x . t) ^2) + ((y . t) ^2) by VALUED_1:5 ;
hence (x (#) y) . t <= (1 / 2) * (((x (#) x) . t) + ((y (#) y) . t)) by A1, Lm5; :: thesis: verum