let f be sequence of REAL; :: thesis: ( f is triangular-valued implies f is integer-valued )
assume A0: f is triangular-valued ; :: thesis: f is integer-valued
for n being object holds f . n is integer

proof

let n be object ; :: thesis: f . n is integer
f . n is triangular by A0;
hence f . n is integer ; :: thesis: verum

end;

hence f is integer-valued by VALUED_0:11; :: thesis: verum