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;

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

hence
F ** (id A) = F
by PBOOLE:3; :: thesis: verumG . i = F . i

let i be object ; :: thesis: ( i in I implies G . b_{1} = F . b_{1} )

assume A1: i in I ; :: thesis: G . b_{1} = F . b_{1}

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 ;

end;assume A1: i in I ; :: thesis: G . 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 ;