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 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
A1: doms f = A and
A2: rngs f c= B ; :: thesis: f is ManySortedFunction of A,B
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or f . i is Element of bool [:(A . i),(B . i):] )
assume A3: 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 A3;
A4: dom (f . s) = A . s by A1, MSSUBFAM:14;
rng (f . s) = (rngs f) . s by MSSUBFAM:13;
then rng (f . s) c= B . s by A2;
hence f . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; :: thesis: verum