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

now :: thesis: ( the carrier of (oContMaps (Y,X)) <> {} & ( for x being Element of (oContMaps (Z,X)) holds G1 . x = G2 . x ) )

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

end;

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