let I1 be set ; :: thesis: for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of
for B being ManySortedSet of st ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) holds
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
for B being ManySortedSet of st ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) holds
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
for B being ManySortedSet of st ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) holds
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of st ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) holds
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
let B be ManySortedSet of ; :: thesis: ( ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) implies for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M )
assume for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ; :: 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

let i be set ; :: 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:21; :: 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:7, FUNCT_2:21;
hence ((id B) * f) . i = id ((B * f) . i) by A3, MSUALG_3:def 1; :: thesis: verum

end;

now

let i be set ; :: thesis: ( i in I1 implies (((id B) * f) ** M) . i = M . i )
assume A4: i in I1 ; :: thesis: (((id B) * f) ** M) . i = M . i
then A5: M . i is Function of (A . i),((B * f) . i) by PBOOLE:def 18;
A6: (B * f) . i = B . (f . i) by A1, A4;
A7: (id B) * f is ManySortedFunction of B * f,B * f

proof

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

end;

( ((id B) * f) . i = (id B) . (f . i) & f . i in I2 ) by A4, FUNCT_2:7, FUNCT_2:21;
then ((id B) * f) . i = id (B . (f . i)) by MSUALG_3:def 1;
hence (((id B) * f) ** M) . i = (id ((B * f) . i)) * (M . i) by A4, A6, A7, MSUALG_3:2
.= M . i by A5, FUNCT_2:23 ;
:: thesis: verum

end;

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