let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
(Funcs) (A,B) is non-empty
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies (Funcs) (A,B) is non-empty )
assume A1: A is_transformable_to B ; :: thesis: (Funcs) (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;
hence Funcs ((A . i),(B . i)) <> {} by FUNCT_2:8; :: thesis: verum

end;

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

proof

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

end;

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