let X be addLoopStr ; :: thesis:
let A, B be Subset of X; :: thesis:
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] )

let x be object ; :: thesis:
assume x in A + B ; :: thesis:
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:
thus y in [:A,B:] by A3, ZFMISC_1:87; :: thesis:
thus S₁[x,y] by A3; :: thesis:

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:
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume A5: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 ) ; :: thesis:
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:

end;