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