deffunc H₂( object ) -> one-to-one Function of (X0 . I),NAT = the one-to-one Function of (X0 . I),NAT;
consider f being ManySortedSet of I such that
A1: for x being object st x in I holds
f . x = H₂(x) from PBOOLE:sch 4();
f is ManySortedFunction of X0,I --> NAT

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in I or f . x is Element of bool [:(X0 . x),((I --> NAT) . x):] )
assume x in I ; :: thesis: f . x is Element of bool [:(X0 . x),((I --> NAT) . x):]
then ( f . x = H₂(x) & (I --> NAT) . x = NAT ) by A1, FUNCOP_1:7;
hence f . x is Element of bool [:(X0 . x),((I --> NAT) . x):] ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of X0,I --> NAT ;
take f ; :: thesis: f is "1-1"
let x be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not x in proj1 f or not f . x = b₁ or b₁ is one-to-one )
let g be Function; :: thesis: ( not x in proj1 f or not f . x = g or g is one-to-one )
assume x in dom f ; :: thesis: ( not f . x = g or g is one-to-one )
then f . x = H₂(x) by A1;
hence ( not f . x = g or g is one-to-one ) ; :: thesis: verum