let I be set ; :: thesis: for A, B, C being non-empty ManySortedSet of I
for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds
f is ManySortedFunction of A,C
let A, B, C be non-empty ManySortedSet of I; :: thesis: for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds
f is ManySortedFunction of A,C
let f be ManySortedFunction of A,B; :: thesis: ( B is ManySortedSubset of C implies f is ManySortedFunction of A,C )
assume A1: B c= C ; :: according to PBOOLE:def 18 :: thesis: f is ManySortedFunction of A,C
let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in I or f . x is Element of bool [:(A . x),(C . x):] )
assume A2: x in I ; :: thesis: f . x is Element of bool [:(A . x),(C . x):]
then A3: ( f . x is Function of (A . x),(B . x) & B . x <> {} & B . x c= C . x ) by A1;
( dom (f . x) = A . x & rng (f . x) c= B . x ) by A2, FUNCT_2:def 1;
hence f . x is Function of (A . x),(C . x) by A3, XBOOLE_1:1, FUNCT_2:2; :: thesis: verum