thus ( f is_less_than g iff for x being Element of X holds f . x <= g . x ) :: thesis: verum

proof

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

assume A1: f is_less_than g ; :: thesis: for x being Element of X holds f . x <= g . x
thus for x being Element of X holds f . x <= g . x :: thesis: verum

proof

let x be Element of X; :: thesis: f . x <= g . x
dom f = X by FUNCT_2:def 1;
hence f . x <= g . x by A1, Def2; :: thesis: verum

end;

end;

assume A2: for x being Element of X holds f . x <= g . x ; :: thesis: f is_less_than g
A3: ( dom f = X & dom g = X ) by FUNCT_2:def 1;
for x being set st x in dom f holds
f . x <= g . x by A2;
hence f is_less_than g by A3, Def2; :: thesis: verum

end;