deffunc H₁( Element of I, Element of I) -> FUNCTION_DOMAIN of Outbds (CPNT . $1), the carrier of (CPNT . $2) = Funcs ((Outbds (CPNT . $1)), the carrier of (CPNT . $2));
set X = XorDelta I;
set Y = union { H₁(i,j) where i, j is Element of I : i <> j } ;
defpred S₁[ object , object ] means ex i, j being Element of I st
( $1 = [i,j] & $2 is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) );
P1: for x being object st x in XorDelta I holds
ex y being object st
( y in union { H₁(i,j) where i, j is Element of I : i <> j } & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in XorDelta I implies ex y being object st
( y in union { H₁(i,j) where i, j is Element of I : i <> j } & S₁[x,y] ) )
assume x in XorDelta I ; :: thesis: ex y being object st
( y in union { H₁(i,j) where i, j is Element of I : i <> j } & S₁[x,y] )
then consider i, j being Element of I such that
P11: ( x = [i,j] & i <> j ) ;
set O12 = the Function of (Outbds (CPNT . i)), the carrier of (CPNT . j);
P12: the Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) in H₁(i,j) by FUNCT_2:8;
H₁(i,j) in { H₁(i,j) where i, j is Element of I : i <> j } by P11;
then the Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) in union { H₁(i,j) where i, j is Element of I : i <> j } by TARSKI:def 4, P12;
hence ex y being object st
( y in union { H₁(i,j) where i, j is Element of I : i <> j } & S₁[x,y] ) by P11; :: thesis: verum

end;

consider f being Function of (XorDelta I),(union { H₁(i,j) where i, j is Element of I : i <> j } ) such that
P2: for x being object st x in XorDelta I holds
S₁[x,f . x] from FUNCT_2:sch 1(P1);
X2: union { H₁(i,j) where i, j is Element of I : i <> j } <> {} by SYLM2;
then reconsider f = f as ManySortedSet of XorDelta I ;
take f ; :: thesis: ( rng f c= union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } & ( for i, j being Element of I st i <> j holds
f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) )
f in Funcs ((XorDelta I),(union { H₁(i,j) where i, j is Element of I : i <> j } )) by X2, FUNCT_2:8;
then ex f0 being Function st
( f = f0 & dom f0 = XorDelta I & rng f0 c= union { H₁(i,j) where i, j is Element of I : i <> j } ) by FUNCT_2:def 2;
hence rng f c= union { H₁(i,j) where i, j is Element of I : i <> j } ; :: thesis: for i, j being Element of I st i <> j holds
f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
thus for i, j being Element of I st i <> j holds
f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) :: thesis: verum

proof

let i, j be Element of I; :: thesis: ( i <> j implies f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) )
assume ASIJ: i <> j ; :: thesis: f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j)
[i,j] in XorDelta I by ASIJ;
then consider i1, j1 being Element of I such that
P4: ( [i,j] = [i1,j1] & f . [i,j] is Function of (Outbds (CPNT . i1)), the carrier of (CPNT . j1) ) by P2;
( i = i1 & j = j1 ) by XTUPLE_0:1, P4;
hence f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by P4; :: thesis: verum

end;