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 set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I1 or (G * f) . i is M5((B * f) . i,(C * f) . i) )
assume A1: i in I1 ; :: thesis: (G * f) . i is M5((B * f) . i,(C * f) . i)
then A2: i in dom f by FUNCT_2:def 1;
then A3: ( B . (f . i) = (B * f) . i & C . (f . i) = (C * f) . i ) by FUNCT_1:23;
G . (f . i) is Function of B . (f . i),C . (f . i) by PBOOLE:def 18, A1, FUNCT_2:7;
hence (G * f) . i is Function of (B * f) . i,(C * f) . i by A2, A3, FUNCT_1:23; :: thesis: verum