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

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

hence
F1 = F2
by FUNCT_2:63; :: thesis: verumlet 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;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