let I1 be set ; :: thesis: for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let I2 be non empty set ; :: thesis: for f being Function of I1,I2
for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let f be Function of I1,I2; :: thesis: for B, C being ManySortedSet of I2
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let B, C be ManySortedSet of I2; :: thesis: for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let G be ManySortedFunction of B,C; :: thesis: G * f is ManySortedFunction of B * f,C * f
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I1 or (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] )
assume A1: i in I1 ; :: thesis: (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):]
then A2: G . (f . i) is Function of (B . (f . i)),(C . (f . i)) by FUNCT_2:5, PBOOLE:def 15;
A3: i in dom f by A1, FUNCT_2:def 1;
then ( B . (f . i) = (B * f) . i & C . (f . i) = (C * f) . i ) by FUNCT_1:13;
hence (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] by A3, A2, FUNCT_1:13; :: thesis: verum