let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F
let A, B be ManySortedSet of I; :: 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 19
.= I /\ (dom F) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I ;
then reconsider G = (id B) ** F as ManySortedFunction of I by PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for i being object st i in I holds
G . i = F . i

let i be object ; :: 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 15;
reconsider g = (id B) . i as Function of (B . i),(B . i) by A1, PBOOLE:def 15;
( g = id (B . i) & G . i = g * f ) by A1, Def1, Th2;
hence G . i = F . i by FUNCT_2:17; :: thesis: verum

end;

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