for o being object st o in dom (REAL --> 1) holds
((sin (#) sin) + (cos (#) cos)) . o = (REAL --> 1) . o

proof

let o be object ; :: thesis: ( o in dom (REAL --> 1) implies ((sin (#) sin) + (cos (#) cos)) . o = (REAL --> 1) . o )
assume A1: o in dom (REAL --> 1) ; :: thesis: ((sin (#) sin) + (cos (#) cos)) . o = (REAL --> 1) . o
then reconsider r = o as Element of REAL ;
A2: ( (sin (#) sin) . r = (sin . r) * (sin . r) & (cos (#) cos) . r = (cos . r) * (cos . r) ) by RFUNCT_1:56;
((sin (#) sin) + (cos (#) cos)) . o = ((sin . r) * (sin . r)) + ((cos . r) * (cos . r)) by A2, RFUNCT_1:56
.= 1 by SIN_COS:28
.= (REAL --> 1) . o by A1, FUNCOP_1:7 ;
hence ((sin (#) sin) + (cos (#) cos)) . o = (REAL --> 1) . o ; :: thesis: verum

end;

then (sin (#) sin) + (cos (#) cos) = REAL --> 1 ;
hence (sin (#) sin) + (cos (#) cos) = 1. (RAlgebra REAL) ; :: thesis: verum