let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
let F be ManySortedFunction of A,B; :: thesis: for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
let X be ManySortedSubset of A; :: thesis: ( F is "1-1" implies F || X is "1-1" )
assume A1: F is "1-1" ; :: thesis: F || X is "1-1"

now :: thesis: for i being set st i in I holds
(F || X) . i is one-to-one

let i be set ; :: thesis: ( i in I implies (F || X) . i is one-to-one )
assume A2: i in I ; :: thesis: (F || X) . i is one-to-one
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
f is one-to-one by A1, A2, MSUALG_3:1;
then f | (X . i) is one-to-one by FUNCT_1:52;
hence (F || X) . i is one-to-one by A2, MSAFREE:def 1; :: thesis: verum

end;

hence F || X is "1-1" by MSUALG_3:1; :: thesis: verum