let I be set ; for A, B, C being V5() 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 V5() ManySortedSet of I; 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; ( B is ManySortedSubset of C implies f is ManySortedFunction of A,C )
assume A1:
B c= C
; PBOOLE:def 18 f is ManySortedFunction of A,C
let x be object ; PBOOLE:def 15 ( not x in I or f . x is Element of bool [:(A . x),(C . x):] )
assume A2:
x in I
; 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; verum