let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
let A, B be ManySortedSet of I; :: 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 :: thesis: for i being object st i in I holds
(F "" B) . i = A . i

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

end;

hence F "" B = A ; :: thesis: verum