deffunc H2( 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 = H2(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 = H2(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 b1 being set holds
( not x in proj1 f or not f . x = b1 or b1 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 = H2(x) by A1;
hence ( not f . x = g or g is one-to-one ) ; :: thesis: verum