deffunc H1( 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 { H1(i,j) where i, j is Element of I : i <> j } ;
defpred S1[ 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 { H1(i,j) where i, j is Element of I : i <> j } & S1[x,y] )
proof
let x be object ; :: thesis: ( x in XorDelta I implies ex y being object st
( y in union { H1(i,j) where i, j is Element of I : i <> j } & S1[x,y] ) )

assume x in XorDelta I ; :: thesis: ex y being object st
( y in union { H1(i,j) where i, j is Element of I : i <> j } & S1[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 H1(i,j) by FUNCT_2:8;
H1(i,j) in { H1(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 { H1(i,j) where i, j is Element of I : i <> j } by ;
hence ex y being object st
( y in union { H1(i,j) where i, j is Element of I : i <> j } & S1[x,y] ) by P11; :: thesis: verum
end;
consider f being Function of (),(union { H1(i,j) where i, j is Element of I : i <> j } ) such that
P2: for x being object st x in XorDelta I holds
S1[x,f . x] from X2: union { H1(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 ((),(union { H1(i,j) where i, j is Element of I : i <> j } )) by ;
then ex f0 being Function st
( f = f0 & dom f0 = XorDelta I & rng f0 c= union { H1(i,j) where i, j is Element of I : i <> j } ) by FUNCT_2:def 2;
hence rng f c= union { H1(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 ;
hence f . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) by P4; :: thesis: verum
end;