let I be set ; :: thesis: for A, B being ManySortedSet of
for F being ManySortedFunction of A,B holds (id B) ** F = F
let A, B be ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B holds (id B) ** F = F
let F be ManySortedFunction of A,B; :: thesis: (id B) ** F = F
dom ((id B) ** F) = (dom (id B)) /\ (dom F) by PBOOLE:def 24
.= I /\ (dom F) by PARTFUN1:def 4
.= I /\ I by PARTFUN1:def 4
.= I ;
then reconsider G = (id B) ** F as ManySortedFunction of by PARTFUN1:def 4, RELAT_1:def 18;

now

let i be set ; :: thesis: ( i in I implies G . i = F . i )
assume A1: i in I ; :: thesis: G . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 18;
reconsider g = (id B) . i as Function of (B . i),(B . i) by A1, PBOOLE:def 18;
A2: g = id (B . i) by A1, Def1;
G . i = g * f by A1, Th2;
hence G . i = F . i by A2, FUNCT_2:23; :: thesis: verum

end;

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