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 4;

now

let i be set ; :: 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, PBOOLE:def 5;
then A6: A . i c= dom (F . i) by A3, A4, FUNCT_6:31;
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 25
.= A . i by A6, A5, FUNCT_1:164 ; :: thesis: verum

end;

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