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 ;
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 . b1 = F . b1 )
assume A1: i in I ; :: thesis: G . b1 = F . b1
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 ;
A2: G . i = f * g by
.= f * (id (A . i)) by ;
per cases not ( B . i = {} & not A . i = {} & not ( B . i = {} & A . i <> {} ) ) ;
suppose ( B . i = {} implies A . i = {} ) ; :: thesis: G . b1 = F . b1
then dom f = A . i by FUNCT_2:def 1;
hence G . i = F . i by ; :: thesis: verum
end;
suppose ( B . i = {} & A . i <> {} ) ; :: thesis: G . b1 = F . b1
then f = {} ;
hence G . i = F . i by A2; :: thesis: verum
end;
end;
end;
hence F ** (id A) = F by PBOOLE:3; :: thesis: verum