let A be Subset of X; :: thesis: ( A = Support f iff for x being Element of X holds
( x in A iff f . x <> 0. S ) )
A1: X = dom f by PARTFUN1:def 2;
hence ( A = Support f implies for x being Element of X holds
( x in A iff f . x <> 0. S ) ) by Def3; :: thesis: ( ( for x being Element of X holds
( x in A iff f . x <> 0. S ) ) implies A = Support f )
assume A2: for x being Element of X holds
( x in A iff f . x <> 0. S ) ; :: thesis: A = Support f
A3: Support f c= dom f by Def3;
thus A c= Support f :: according to XBOOLE_0:def 10 :: thesis: Support f c= A
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in Support f )
assume A4: e in A ; :: thesis: e in Support f
then f . e <> 0. S by A2;
hence e in Support f by A4, A1, Def3; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Support f or e in A )
assume A5: e in Support f ; :: thesis: e in A
then A6: f . e <> 0. S by Def3;
Support f c= X by A3, XBOOLE_1:1;
hence e in A by A2, A6, A5; :: thesis: verum