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 ;
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 ; :: 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 ; :: thesis: verum