let A be Preorder; :: thesis: for f being finite-support Function of A,REAL st f is nonnegative-yielding holds
(proj A) .: () = support ()

let f be finite-support Function of the carrier of A,REAL; :: thesis: ( f is nonnegative-yielding implies (proj A) .: () = support () )
assume A1: f is nonnegative-yielding ; :: thesis: (proj A) .: () = support ()
for X being object st X in (proj A) .: () holds
X in support ()
proof
let X be object ; :: thesis: ( X in (proj A) .: () implies X in support () )
assume A2: X in (proj A) .: () ; :: thesis: X in support ()
then consider x being object such that
A3: x in dom (proj A) and
A4: x in support f and
A5: X = (proj A) . x by FUNCT_1:def 6;
A6: X in the carrier of () by ;
reconsider Y = X as Element of the carrier of () by A6;
set s = canFS (eqSupport (f,Y));
A7: rng (canFS (eqSupport (f,Y))) = eqSupport (f,Y) by FUNCT_2:def 3;
canFS (eqSupport (f,Y)) is FinSequence of the carrier of A by FINSEQ_2:24;
then reconsider fs = f * (canFS (eqSupport (f,Y))) as FinSequence of REAL by FINSEQ_2:32;
A8: ex k being Nat st
( k in dom fs & fs . k <> 0 )
proof
reconsider y = x as Element of A by A3;
X = Class ((),y) by ;
then y in Y by ;
then y in eqSupport (f,Y) by ;
then consider i being object such that
A9: i in dom (canFS (eqSupport (f,Y))) and
A10: (canFS (eqSupport (f,Y))) . i = y by ;
reconsider i = i as Nat by A9;
take i ; :: thesis: ( i in dom fs & fs . i <> 0 )
thus i in dom fs by ; :: thesis: fs . i <> 0
f . y <> 0 by ;
hence fs . i <> 0 by ; :: thesis: verum
end;
A11: (eqSumOf f) . Y = Sum fs by ;
Sum fs > 0 by A1, A8, Th7;
hence X in support () by ; :: thesis: verum
end;
then (proj A) .: () c= support () ;
hence (proj A) .: () = support () by Th63; :: thesis: verum