Affin
A
=
{
(
Sum
L
)
where
L
is
Linear_Combination
of
A
:
sum
L
=
1
}
by
Th59
;
hence
ex
b
_{1}
being
Linear_Combination
of
A
st
(
Sum
b
_{1}
=
x
&
sum
b
_{1}
=
1 )
by
A2
;
:: thesis:
verum