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

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