let S1, S2 be IncProjStr ; :: thesis: for F being IncProjMap over 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 over 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 object ; :: 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 consider A being POINT of S1 such that
A3: a = A ;
A4: the point-map of F . a in K by A2, FUNCT_1:def 7;
then consider B1 being POINT of S2 such that
A5: the point-map of F . a = B1 ;
F . A = B1 by A3, 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 A4, A3; :: 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 object ; :: 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 A6: ex A being POINT of S1 st
( 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 7; :: 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