let X be non empty set ; :: thesis: for T being non empty RelStr
for f, g being Element of (T |^ X) holds
( f <= g iff for x being Element of X holds f . x <= g . x )
let T be non empty RelStr ; :: thesis: for f, g being Element of (T |^ X) holds
( f <= g iff for x being Element of X holds f . x <= g . x )
let f, g be Element of (T |^ X); :: thesis: ( f <= g iff for x being Element of X holds f . x <= g . x )
reconsider a = f, b = g as Element of (product (X --> T)) by YELLOW_1:def 5;
A1: T |^ X = product (X --> T) by YELLOW_1:def 5;

hereby :: thesis: ( ( for x being Element of X holds f . x <= g . x ) implies f <= g )

assume A2: f <= g ; :: thesis: for x being Element of X holds f . x <= g . x
let x be Element of X; :: thesis: f . x <= g . x
(X --> T) . x = T ;
hence f . x <= g . x by A1, A2, WAYBEL_3:28; :: thesis: verum

end;

assume for x being Element of X holds f . x <= g . x ; :: thesis: f <= g
then for x being Element of X holds a . x <= b . x ;
hence f <= g by A1, WAYBEL_3:28; :: thesis: verum