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 :: thesis: ( the carrier of (oContMaps (X,Z)) <> {} & ( for x being Element of (oContMaps (X,Y)) holds G1 . x = G2 . x ) )

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:63; :: thesis: verum