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

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

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