let A be Preorder; :: thesis: for f being finite-support Function of A,REAL holds support () c= (proj A) .: ()
let f be finite-support Function of the carrier of A,REAL; :: thesis: support () c= (proj A) .: ()
for X being object st X in support () holds
X in (proj A) .: ()
proof
let X be object ; :: thesis: ( X in support () implies X in (proj A) .: () )
assume A1: X in support () ; :: thesis: X in (proj A) .: ()
ex x being object st
( x in dom (proj A) & x in support f & X = (proj A) . x )
proof
X in dom () by A1;
then A2: X in the carrier of () ;
A3: dom (proj A) = the carrier of A by ;
reconsider Y = X as Element of () by A2;
set s = canFS (eqSupport (f,Y));
A4: rng (canFS (eqSupport (f,Y))) c= eqSupport (f,Y) by FINSEQ_1:def 4;
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;
(eqSumOf f) . Y <> 0 by ;
then Sum fs <> 0 by ;
then consider i being Nat such that
A5: i in dom fs and
A6: fs . i <> 0 by Th6;
A7: ( i in dom (canFS (eqSupport (f,Y))) & (canFS (eqSupport (f,Y))) . i in dom f ) by ;
then reconsider x = (canFS (eqSupport (f,Y))) . i as Element of A ;
take x ; :: thesis: ( x in dom (proj A) & x in support f & X = (proj A) . x )
thus x in dom (proj A) by A3, A7; :: thesis: ( x in support f & X = (proj A) . x )
f . x <> 0 by ;
hence x in support f by PRE_POLY:def 7; :: thesis: X = (proj A) . x
x in eqSupport (f,Y) by ;
then A8: x in Y by ;
X in Class () by ;
then consider y being object such that
A9: y in the carrier of A and
A10: X = Class ((),y) by EQREL_1:def 3;
A11: x in Class ((),y) by ;
thus (proj A) . x = Class ((),x) by Def8
.= X by ; :: thesis: verum
end;
hence X in (proj A) .: () by FUNCT_1:def 6; :: thesis: verum
end;
hence support () c= (proj A) .: () ; :: thesis: verum