let I be set ; :: thesis: for A, B being ManySortedSet of
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
let A, B be ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
let F be ManySortedFunction of A,B; :: thesis: ( A is_transformable_to B implies F "" B = A )
assume A1: A is_transformable_to B ; :: thesis: F "" B = A

now

let i be set ; :: thesis: ( i in I implies (F "" B) . i = A . i )
assume A2: i in I ; :: thesis: (F "" B) . i = A . i
then A3: ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def 3;
A4: F . i is Function of (A . i),(B . i) by A2, PBOOLE:def 18;
thus (F "" B) . i = (F . i) " (B . i) by A2, Def1
.= A . i by A3, A4, FUNCT_2:48 ; :: thesis: verum

end;

hence F "" B = A by PBOOLE:3; :: thesis: verum