let I1 be set ; :: thesis: for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let I2 be non empty set ; :: thesis: for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let f be Function of I1,I2; :: thesis: for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let A be ManySortedSet of I1; :: thesis: for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let B be ManySortedSet of I2; :: thesis: for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let M be ManySortedFunction of A,B * f; :: thesis: ((id B) * f) ** M = M

A1: now :: thesis: for i being object st i in I1 holds
( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) )

let i be object ; :: thesis: ( i in I1 implies ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) ) )
assume A2: i in I1 ; :: thesis: ( (B * f) . i = B . (f . i) & ((id B) * f) . i = id ((B * f) . i) )
hence A3: (B * f) . i = B . (f . i) by FUNCT_2:15; :: thesis: ((id B) * f) . i = id ((B * f) . i)
( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A2, FUNCT_2:5, FUNCT_2:15;
hence ((id B) * f) . i = id ((B * f) . i) by A3, MSUALG_3:def 1; :: thesis: verum

end;

now :: thesis: for i being object st i in I1 holds
(((id B) * f) ** M) . i = M . i

A4: (id B) * f is ManySortedFunction of B * f,B * f

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I1 or ((id B) * f) . i is M3( bool [:((B * f) . i),((B * f) . i):]) )
assume i in I1 ; :: thesis: ((id B) * f) . i is M3( bool [:((B * f) . i),((B * f) . i):])
then ((id B) * f) . i = id ((B * f) . i) by A1;
hence ((id B) * f) . i is M3( bool [:((B * f) . i),((B * f) . i):]) ; :: thesis: verum

end;

let i be object ; :: thesis: ( i in I1 implies (((id B) * f) ** M) . i = M . i )
assume A5: i in I1 ; :: thesis: (((id B) * f) ** M) . i = M . i
then A6: M . i is Function of (A . i),((B * f) . i) by PBOOLE:def 15;
( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A5, FUNCT_2:5, FUNCT_2:15;
then A7: ((id B) * f) . i = id (B . (f . i)) by MSUALG_3:def 1;
(B * f) . i = B . (f . i) by A1, A5;
hence (((id B) * f) ** M) . i = (id ((B * f) . i)) * (M . i) by A5, A4, A7, MSUALG_3:2
.= M . i by A6, FUNCT_2:17 ;
:: thesis: verum

end;

hence ((id B) * f) ** M = M ; :: thesis: verum