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