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