let X be addLoopStr ; :: thesis: for A, B being Subset of X ex F being Function of (A + B),[:A,B:] st F is one-to-one

let A, B be Subset of X; :: thesis: ex F being Function of (A + B),[:A,B:] st F is one-to-one

set D = A + B;

defpred S_{1}[ object , object ] means ex a, b being Point of X st

( $1 = a + b & a in A & b in B & $2 = [a,b] );

A2: for x being object st x in A + B holds

ex y being object st

( y in [:A,B:] & S_{1}[x,y] )

A4: for x being object st x in A + B holds

S_{1}[x,F . x]
from FUNCT_2:sch 1(A2);

take F ; :: thesis: F is one-to-one

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

let A, B be Subset of X; :: thesis: ex F being Function of (A + B),[:A,B:] st F is one-to-one

set D = A + B;

defpred S

( $1 = a + b & a in A & b in B & $2 = [a,b] );

A2: for x being object st x in A + B holds

ex y being object st

( y in [:A,B:] & S

proof

consider F being Function of (A + B),[:A,B:] such that
let x be object ; :: thesis: ( x in A + B implies ex y being object st

( y in [:A,B:] & S_{1}[x,y] ) )

assume x in A + B ; :: thesis: ex y being object st

( y in [:A,B:] & S_{1}[x,y] )

then x in { (a + b) where a, b is Element of X : ( a in A & b in B ) } by IDEAL_1:def 19;

then consider a, b being Element of X such that

A3: ( x = a + b & a in A & b in B ) ;

take y = [a,b]; :: thesis: ( y in [:A,B:] & S_{1}[x,y] )

thus y in [:A,B:] by A3, ZFMISC_1:87; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;( y in [:A,B:] & S

assume x in A + B ; :: thesis: ex y being object st

( y in [:A,B:] & S

then x in { (a + b) where a, b is Element of X : ( a in A & b in B ) } by IDEAL_1:def 19;

then consider a, b being Element of X such that

A3: ( x = a + b & a in A & b in B ) ;

take y = [a,b]; :: thesis: ( y in [:A,B:] & S

thus y in [:A,B:] by A3, ZFMISC_1:87; :: thesis: S

thus S

A4: for x being object st x in A + B holds

S

take F ; :: thesis: F is one-to-one

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

proof

hence
F is one-to-one
; :: thesis: verum
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )

assume A5: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2

then A6: ex a1, b1 being Point of X st

( x1 = a1 + b1 & a1 in A & b1 in B & F . x1 = [a1,b1] ) by A4;

ex a2, b2 being Point of X st

( x2 = a2 + b2 & a2 in A & b2 in B & F . x2 = [a2,b2] ) by A4, A5;

hence x1 = x2 by A5, A6; :: thesis: verum

end;assume A5: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis: x1 = x2

then A6: ex a1, b1 being Point of X st

( x1 = a1 + b1 & a1 in A & b1 in B & F . x1 = [a1,b1] ) by A4;

ex a2, b2 being Point of X st

( x2 = a2 + b2 & a2 in A & b2 in B & F . x2 = [a2,b2] ) by A4, A5;

hence x1 = x2 by A5, A6; :: thesis: verum