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 ) }
proof
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;
{ B where B is POINT of S2 : ex A being POINT of S1 st
( A in K & F . A = B ) } c= F .: K
proof
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;
hence F .: K = { B where B is POINT of S2 : ex A being POINT of S1 st
( A in K & F . A = B ) } by A1, XBOOLE_0:def 10; :: thesis: verum