let G1, G2 be Function of (oContMaps X,Y),(oContMaps X,Z); :: thesis: ( ( for g being continuous Function of X,Y holds G1 . g = f * g ) & ( for g being continuous Function of X,Y holds G2 . g = f * g ) implies G1 = G2 )
assume that
A1: for g being continuous Function of X,Y holds G1 . g = f * g and
A2: for g being continuous Function of X,Y holds G2 . g = f * g ; :: thesis: G1 = G2

now

thus the carrier of (oContMaps X,Z) <> {} ; :: thesis: for x being Element of (oContMaps X,Y) holds G1 . x = G2 . x
let x be Element of (oContMaps X,Y); :: thesis: G1 . x = G2 . x
reconsider g = x as continuous Function of X,Y by Th2;
thus G1 . x = f * g by A1
.= G2 . x by A2 ; :: thesis: verum

end;

hence G1 = G2 by FUNCT_2:113; :: thesis: verum