let l1, l2 be Element of F; :: thesis: ( ( for l being Element of F st a _|_ holds

l1 = l ) & ( for l being Element of F st a _|_ holds

l2 = l ) implies l1 = l2 )

assume that

A3: for l being Element of F st a _|_ holds

l1 = l and

A4: for l being Element of F st a _|_ holds

l2 = l ; :: thesis: l1 = l2

consider k being Element of F such that

A5: a _|_ by A1, Def1;

l1 = k by A3, A5;

hence l1 = l2 by A4, A5; :: thesis: verum

l1 = l ) & ( for l being Element of F st a _|_ holds

l2 = l ) implies l1 = l2 )

assume that

A3: for l being Element of F st a _|_ holds

l1 = l and

A4: for l being Element of F st a _|_ holds

l2 = l ; :: thesis: l1 = l2

consider k being Element of F such that

A5: a _|_ by A1, Def1;

l1 = k by A3, A5;

hence l1 = l2 by A4, A5; :: thesis: verum