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;

now :: thesis: for i being object st i in I holds
(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;

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