let X be addLoopStr ; 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; 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 ;
( x in A + B implies ex y being object st
( y in [:A,B:] & S1[x,y] ) )
assume
x in A + B
;
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];
( y in [:A,B:] & S1[x,y] )
thus
y in [:A,B:]
by A3, ZFMISC_1:87;
S1[x,y]
thus
S1[
x,
y]
by A3;
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 FUNCT_2:sch 1(A2);
take
F
; 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
hence
F is one-to-one
; verum