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;

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

hence
(id B) ** F = F
by PBOOLE:3; :: thesis: verumG . 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;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