let S1, S2 be IncProjStr ; :: thesis: for F being IncProjMap of S1,S2
for K being Subset of the Points of S2 holds F " K = { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) }
let F be IncProjMap of S1,S2; :: thesis: for K being Subset of the Points of S2 holds F " K = { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) }
let K be Subset of the Points of S2; :: thesis: F " K = { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) }
set Image = { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } ;
A1: F " K c= { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in F " K or a in { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } )
assume A2: a in F " K ; :: thesis: a in { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) }
then A3: ( a in dom the point-map of F & the point-map of F . a in K ) by FUNCT_1:def 13;
consider A being POINT of S1 such that
A4: a = A by A2;
consider B1 being POINT of S2 such that
A5: the point-map of F . a = B1 by A3;
F . A = B1 by A4, A5;
hence a in { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } by A3, A4; :: thesis: verum

end;

{ A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } c= F " K

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } or a in F " K )
assume a in { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } ; :: thesis: a in F " K
then consider A being POINT of S1 such that
A6: ( A = a & ex B being POINT of S2 st
( B in K & F . A = B ) ) ;
the Points of S1 = dom the point-map of F by FUNCT_2:def 1;
hence a in F " K by A6, FUNCT_1:def 13; :: thesis: verum

end;

hence F " K = { A where A is POINT of S1 : ex B being POINT of S2 st
( B in K & F . A = B ) } by A1, XBOOLE_0:def 10; :: thesis: verum