let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B )
assume A1: for i being set st i in I & B . i = {} holds
A . i = {} ; :: according to PZFMISC1:def 3 :: thesis: for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B
let f be ManySortedFunction of I; :: thesis: ( doms f = A & rngs f c= B implies f is ManySortedFunction of A,B )
assume that
A2: doms f = A and
A3: rngs f c= B ; :: thesis: f is ManySortedFunction of A,B
let i be set ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or f . i is Element of bool [:(A . i),(B . i):] )
assume A4: i in I ; :: thesis: f . i is Element of bool [:(A . i),(B . i):]
then reconsider J = I as non empty set ;
reconsider s = i as Element of J by A4;
A5: dom (f . s) = A . s by A2, MSSUBFAM:14;
rng (f . s) = (rngs f) . s by MSSUBFAM:13;
then A6: rng (f . s) c= B . s by A3, PBOOLE:def 2;
( B . s = {} implies A . s = {} ) by A1;
hence f . i is Element of bool [:(A . i),(B . i):] by A5, A6, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum