let I be set ; :: thesis: for A being ManySortedSet of I

for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

let A be ManySortedSet of I; :: thesis: for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

let F be ManySortedFunction of I; :: thesis: ( F is "1-1" & A c= doms F implies F "" (F .:.: A) = A )

assume that

A1: F is "1-1" and

A2: A c= doms F ; :: thesis: F "" (F .:.: A) = A

A3: dom F = I by PARTFUN1:def 2;

for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

let A be ManySortedSet of I; :: thesis: for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

let F be ManySortedFunction of I; :: thesis: ( F is "1-1" & A c= doms F implies F "" (F .:.: A) = A )

assume that

A1: F is "1-1" and

A2: A c= doms F ; :: thesis: F "" (F .:.: A) = A

A3: dom F = I by PARTFUN1:def 2;

now :: thesis: for i being object st i in I holds

(F "" (F .:.: A)) . i = A . i

hence
F "" (F .:.: A) = A
; :: thesis: verum(F "" (F .:.: A)) . i = A . i

let i be object ; :: thesis: ( i in I implies (F "" (F .:.: A)) . i = A . i )

assume A4: i in I ; :: thesis: (F "" (F .:.: A)) . i = A . i

then A5: F . i is one-to-one by A1, A3, MSUALG_3:def 2;

A . i c= (doms F) . i by A2, A4;

then A6: A . i c= dom (F . i) by A3, A4, FUNCT_6:22;

thus (F "" (F .:.: A)) . i = (F . i) " ((F .:.: A) . i) by A4, EQUATION:def 1

.= (F . i) " ((F . i) .: (A . i)) by A4, PBOOLE:def 20

.= A . i by A6, A5, FUNCT_1:94 ; :: thesis: verum

end;assume A4: i in I ; :: thesis: (F "" (F .:.: A)) . i = A . i

then A5: F . i is one-to-one by A1, A3, MSUALG_3:def 2;

A . i c= (doms F) . i by A2, A4;

then A6: A . i c= dom (F . i) by A3, A4, FUNCT_6:22;

thus (F "" (F .:.: A)) . i = (F . i) " ((F .:.: A) . i) by A4, EQUATION:def 1

.= (F . i) " ((F . i) .: (A . i)) by A4, PBOOLE:def 20

.= A . i by A6, A5, FUNCT_1:94 ; :: thesis: verum