let S1, S2 be IncProjStr ; :: thesis: for F being IncProjMap over S1,S2

for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

let F be IncProjMap over S1,S2; :: thesis: for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

let K be Subset of the Points of S1; :: thesis: F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

set Image = { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } ;

A1: F .: K c= { B where B is POINT of S2 : ex A being POINT of S1 st

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

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

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

for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

let F be IncProjMap over S1,S2; :: thesis: for K being Subset of the Points of S1 holds F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

let K be Subset of the Points of S1; :: thesis: F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st

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

set Image = { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } ;

A1: F .: K c= { B where B is POINT of S2 : ex A being POINT of S1 st

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

proof

{ B where B is POINT of S2 : ex A being POINT of S1 st
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in F .: K or b in { B where B is POINT of S2 : ex A being POINT of S1 st

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

assume b in F .: K ; :: thesis: b in { B where B is POINT of S2 : ex A being POINT of S1 st

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

then consider a being object such that

A2: a in dom the point-map of F and

A3: a in K and

A4: b = the point-map of F . a by FUNCT_1:def 6;

consider A being POINT of S1 such that

A5: a = A by A2;

b in the Points of S2 by A2, A4, FUNCT_2:5;

then consider B1 being POINT of S2 such that

A6: b = B1 ;

F . A = B1 by A4, A5, A6;

hence b in { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } by A3, A4, A5; :: thesis: verum

end;( A in K & F . A = B ) } )

assume b in F .: K ; :: thesis: b in { B where B is POINT of S2 : ex A being POINT of S1 st

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

then consider a being object such that

A2: a in dom the point-map of F and

A3: a in K and

A4: b = the point-map of F . a by FUNCT_1:def 6;

consider A being POINT of S1 such that

A5: a = A by A2;

b in the Points of S2 by A2, A4, FUNCT_2:5;

then consider B1 being POINT of S2 such that

A6: b = B1 ;

F . A = B1 by A4, A5, A6;

hence b in { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } by A3, A4, A5; :: thesis: verum

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

proof

hence
F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } or b in F .: K )

assume b in { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } ; :: thesis: b in F .: K

then A7: ex B being POINT of S2 st

( B = b & ex A being POINT of S1 st

( A in K & F . A = B ) ) ;

the Points of S1 = dom the point-map of F by FUNCT_2:def 1;

hence b in F .: K by A7, FUNCT_1:def 6; :: thesis: verum

end;( A in K & F . A = B ) } or b in F .: K )

assume b in { B where B is POINT of S2 : ex A being POINT of S1 st

( A in K & F . A = B ) } ; :: thesis: b in F .: K

then A7: ex B being POINT of S2 st

( B = b & ex A being POINT of S1 st

( A in K & F . A = B ) ) ;

the Points of S1 = dom the point-map of F by FUNCT_2:def 1;

hence b in F .: K by A7, FUNCT_1:def 6; :: thesis: verum

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