consider a, b being Real such that
A1: u = (a * w) + (b * y) by B1, ANALMETR:def 1;
take b ; :: thesis: ex a being Real st u = (a * w) + (b * y)
thus ex a being Real st u = (a * w) + (b * y) by A1; :: thesis: verum