deffunc H_{1}( 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_{1}(i,j) where i, j is Element of I : i <> j } ;

defpred S_{1}[ 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_{1}(i,j) where i, j is Element of I : i <> j } & S_{1}[x,y] )
_{1}(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_{1}[x,f . x]
from FUNCT_2:sch 1(P1);

X2: union { H_{1}(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_{1}(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_{1}(i,j) where i, j is Element of I : i <> j } )
by FUNCT_2:def 2;

hence rng f c= union { H_{1}(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

set X = XorDelta I;

set Y = union { H

defpred S

( $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

proof

consider f being Function of (XorDelta I),(union { H
let x be object ; :: thesis: ( x in XorDelta I implies ex y being object st

( y in union { H_{1}(i,j) where i, j is Element of I : i <> j } & S_{1}[x,y] ) )

assume x in XorDelta I ; :: thesis: ex y being object st

( y in union { H_{1}(i,j) where i, j is Element of I : i <> j } & S_{1}[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_{1}(i,j)
by FUNCT_2:8;

H_{1}(i,j) in { H_{1}(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_{1}(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_{1}(i,j) where i, j is Element of I : i <> j } & S_{1}[x,y] )
by P11; :: thesis: verum

end;( y in union { H

assume x in XorDelta I ; :: thesis: ex y being object st

( y in union { H

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

H

then the Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) in union { H

hence ex y being object st

( y in union { H

P2: for x being object st x in XorDelta I holds

S

X2: union { H

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

then ex f0 being Function st

( f = f0 & dom f0 = XorDelta I & rng f0 c= union { H

hence rng f c= union { H

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;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