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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in A + B implies ex y being object st
( y in [:A,B:] & S₁[x,y] ) )
assume x in A + B ; :: thesis: ex y being object st
( y in [:A,B:] & S₁[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₁[x,y] )
thus y in [:A,B:] by A3, ZFMISC_1:87; :: thesis: S₁[x,y]
thus S₁[x,y] by A3; :: thesis: verum

end;

consider F being Function of (A + B),[:A,B:] such that
A4: for x being object st x in A + B holds
S₁[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

proof

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;

hence F is one-to-one ; :: thesis: verum