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

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 ) )

hence
G1 = G2
by FUNCT_2:63; :: thesis: verumthus
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;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