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

now

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

per cases not ( B . i = {} & not A . i = {} & not ( B . i = {} & A . i <> {} ) ) ;

suppose ( B . i = {} implies A . i = {} ) ; :: thesis: G . b₁ = F . b₁

then dom f = A . i by FUNCT_2:def 1;
hence G . i = F . i by A2, RELAT_1:78; :: thesis: verum

end;

suppose ( B . i = {} & A . i <> {} ) ; :: thesis: G . b₁ = F . b₁

then f = {} ;
hence G . i = F . i by A2; :: thesis: verum

end;

end;

end;

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