let I be set ; :: thesis: for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A
let A be ManySortedSet of I; :: thesis: for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A
let F be ManySortedFunction of I; :: thesis: ( A c= rngs F implies F .:.: (F "" A) = A )
assume A1: A c= rngs F ; :: thesis: F .:.: (F "" A) = A

now

let i be set ; :: thesis: ( i in I implies (F .:.: (F "" A)) . i = A . i )
assume A2: i in I ; :: thesis: (F .:.: (F "" A)) . i = A . i
then A . i c= (rngs F) . i by A1, PBOOLE:def 5;
then A3: A . i c= rng (F . i) by A2, MSSUBFAM:13;
thus (F .:.: (F "" A)) . i = (F . i) .: ((F "" A) . i) by A2, PBOOLE:def 25
.= (F . i) .: ((F . i) " (A . i)) by A2, Def1
.= A . i by A3, FUNCT_1:147 ; :: thesis: verum

end;

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