consider a, b being Real such that
A2: u = (a * w) + (b * y) by A1, 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 A2; :: thesis: verum