let F1, F2 be Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M); :: thesis: ( ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F2 . f = commute f ) implies F1 = F2 )
assume that
A1: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F1 . f = commute f and
A2: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F2 . f = commute f ; :: thesis: F1 = F2

now :: thesis: for f being Element of (oContMaps (X,(M -TOP_prod (M => Y)))) holds F1 . f = F2 . f

let f be Element of (oContMaps (X,(M -TOP_prod (M => Y)))); :: thesis: F1 . f = F2 . f
reconsider g = f as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:2;
thus F1 . f = commute g by A1
.= F2 . f by A2 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum