let I be set ; 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; ( 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 = {}
; PZFMISC1:def 3 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; ( 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
; f is ManySortedFunction of A,B
let i be object ; PBOOLE:def 15 ( not i in I or f . i is Element of bool [:(A . i),(B . i):] )
assume A3:
i in I
; 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; verum