let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
MSFuncs A,B is non-empty
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies MSFuncs A,B is non-empty )
assume A1: A is_transformable_to B ; :: thesis: MSFuncs A,B is non-empty
A2: for i being set st i in I holds
Funcs (A . i),(B . i) <> {}

proof

let i be set ; :: thesis: ( i in I implies Funcs (A . i),(B . i) <> {} )
assume i in I ; :: thesis: Funcs (A . i),(B . i) <> {}
then ( B . i = {} implies A . i = {} ) by A1, PZFMISC1:def 3;
hence Funcs (A . i),(B . i) <> {} by FUNCT_2:11; :: thesis: verum

end;

for i being set st i in I holds
(MSFuncs A,B) . i <> {}

proof

let i be set ; :: thesis: ( i in I implies (MSFuncs A,B) . i <> {} )
assume A3: i in I ; :: thesis: (MSFuncs A,B) . i <> {}
then (MSFuncs A,B) . i = Funcs (A . i),(B . i) by PBOOLE:def 22;
hence (MSFuncs A,B) . i <> {} by A2, A3; :: thesis: verum

end;

then for i being set st i in I holds
not (MSFuncs A,B) . i is empty ;
hence MSFuncs A,B is non-empty by PBOOLE:def 16; :: thesis: verum