let X, Y be non empty TopSpace; :: thesis: for a, b being Element of (oContMaps (X,Y))

for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

let a, b be Element of (oContMaps (X,Y)); :: thesis: for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

A1: oContMaps (X,Y) is full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;

then reconsider x = a, y = b as Element of ((Omega Y) |^ the carrier of X) by YELLOW_0:58;

A2: ( a <= b iff x <= y ) by A1, YELLOW_0:59, YELLOW_0:60;

let f, g be Function of X,(Omega Y); :: thesis: ( a = f & b = g implies ( a <= b iff f <= g ) )

assume ( a = f & b = g ) ; :: thesis: ( a <= b iff f <= g )

hence ( a <= b iff f <= g ) by A2, WAYBEL10:11; :: thesis: verum

for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

let a, b be Element of (oContMaps (X,Y)); :: thesis: for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

A1: oContMaps (X,Y) is full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;

then reconsider x = a, y = b as Element of ((Omega Y) |^ the carrier of X) by YELLOW_0:58;

A2: ( a <= b iff x <= y ) by A1, YELLOW_0:59, YELLOW_0:60;

let f, g be Function of X,(Omega Y); :: thesis: ( a = f & b = g implies ( a <= b iff f <= g ) )

assume ( a = f & b = g ) ; :: thesis: ( a <= b iff f <= g )

hence ( a <= b iff f <= g ) by A2, WAYBEL10:11; :: thesis: verum