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