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 ) }

( B in K & F . A = B ) } c= F " K

( B in K & F . A = B ) } by A1, XBOOLE_0:def 10; :: thesis: verum

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

{ A where A is POINT of S1 : ex B being POINT of S2 st
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;( 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

( B in K & F . A = B ) } c= F " K

proof

hence
F " K = { A where A is POINT of S1 : ex B being POINT of S2 st
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;( 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

( B in K & F . A = B ) } by A1, XBOOLE_0:def 10; :: thesis: verum