let p, q, r be FinSequence of REAL ; :: thesis: ( r = p ^ q & ( for x being Real st x in rng r holds
x >= 0 ) implies ( ( for i being Nat st i in dom p holds
p . i >= 0 ) & ( for i being Nat st i in dom q holds
q . i >= 0 ) ) )
assume that
A1: r = p ^ q and
A2: for x being Real st x in rng r holds
x >= 0 ; :: thesis: ( ( for i being Nat st i in dom p holds
p . i >= 0 ) & ( for i being Nat st i in dom q holds
q . i >= 0 ) )
rng p c= rng r by A1, FINSEQ_1:29;
then for y being Real st y in rng p holds
y >= 0 by A2;
hence for i being Nat st i in dom p holds
p . i >= 0 by Lm3; :: thesis: for i being Nat st i in dom q holds
q . i >= 0
rng q c= rng r by A1, FINSEQ_1:30;
then for y being Real st y in rng q holds
y >= 0 by A2;
hence for i being Nat st i in dom q holds
q . i >= 0 by Lm3; :: thesis: verum