let f be Function; :: thesis: for I being set

for A, B being ManySortedSet of I st ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) holds

f -MSF (I,A) is ManySortedFunction of A,B

let I be set ; :: thesis: for A, B being ManySortedSet of I st ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) holds

f -MSF (I,A) is ManySortedFunction of A,B

let A, B be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) implies f -MSF (I,A) is ManySortedFunction of A,B )

assume A1: for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ; :: thesis: f -MSF (I,A) is ManySortedFunction of A,B

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] )

assume A2: i in I ; :: thesis: (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):]

then A3: (f -MSF (I,A)) . i = f | (A . i) by Def1;

f .: (A . i) c= B . i by A1, A2;

then A4: rng ((f -MSF (I,A)) . i) c= B . i by A3, RELAT_1:115;

dom ((f -MSF (I,A)) . i) = A . i by A1, A2, A3, RELAT_1:62;

hence (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; :: thesis: verum

for A, B being ManySortedSet of I st ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) holds

f -MSF (I,A) is ManySortedFunction of A,B

let I be set ; :: thesis: for A, B being ManySortedSet of I st ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) holds

f -MSF (I,A) is ManySortedFunction of A,B

let A, B be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ) implies f -MSF (I,A) is ManySortedFunction of A,B )

assume A1: for i being set st i in I holds

( A . i c= dom f & f .: (A . i) c= B . i ) ; :: thesis: f -MSF (I,A) is ManySortedFunction of A,B

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] )

assume A2: i in I ; :: thesis: (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):]

then A3: (f -MSF (I,A)) . i = f | (A . i) by Def1;

f .: (A . i) c= B . i by A1, A2;

then A4: rng ((f -MSF (I,A)) . i) c= B . i by A3, RELAT_1:115;

dom ((f -MSF (I,A)) . i) = A . i by A1, A2, A3, RELAT_1:62;

hence (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; :: thesis: verum