let I1 be set ; :: thesis: for I2 being non empty set
for f being Function of I1,I2
for B, C being ManySortedSet of
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
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
for G being ManySortedFunction of B,C holds G * f is ManySortedFunction of B * f,C * f
let B, C be ManySortedSet of ; :: 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 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: 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 A1, FUNCT_2:7, PBOOLE:def 18;
hence (G * f) . i is Element of bool [:((B * f) . i),((C * f) . i):] by A2, A3, FUNCT_1:23; :: thesis: verum