let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (f *' g) or y in INT )
assume y in rng (f *' g) ; :: thesis: y in INT
then consider x being object such that
A5: x in dom (f *' g) and
A6: (f *' g) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A5;
consider r being FinSequence of F_Real such that
len r = x + 1 and
A7: (f *' g) . x = Sum r and
A8: for k being Element of NAT st k in dom r holds
r . k = (f . (k -' 1)) * (g . ((x + 1) -' k)) by POLYNOM3:def 9;
r is INT -valued
proof
let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng r or y in INT )
assume y in rng r ; :: thesis: y in INT
then consider a being object such that
A9: a in dom r and
A10: r . a = y by FUNCT_1:def 3;
reconsider a = a as Element of NAT by A9;
r . a = (f . (a -' 1)) * (g . ((x + 1) -' a)) by A8, A9;
hence y in INT by A10, INT_1:def 2; :: thesis: verum
end;
hence y in INT by A6, A7, INT_1:def 2; :: thesis: verum