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 S1[ 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:] & S1[x,y] )
proof
let x be object ; :: thesis: ( x in A + B implies ex y being object st
( y in [:A,B:] & S1[x,y] ) )

assume x in A + B ; :: thesis: ex y being object st
( y in [:A,B:] & S1[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:] & S1[x,y] )
thus y in [:A,B:] by ; :: thesis: S1[x,y]
thus S1[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
S1[x,F . x] from 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