let c1, c2 be Number ; ( ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & c1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & c2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) implies c1 = c2 )
given y1, y2, y3, y4 being Real such that A2:
y = [*y1,y2,y3,y4*]
and
A3:
c1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*]
; ( for y1, y2, y3, y4 being Real holds
( not y = [*y1,y2,y3,y4*] or not c2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) or c1 = c2 )
given y19, y29, y39, y49 being Real such that A4:
y = [*y19,y29,y39,y49*]
and
A5:
c2 = [*(x * y19),(x * y29),(x * y39),(x * y49)*]
; c1 = c2
A6:
y1 = y19
by A2, A4, Th5;
A7:
y2 = y29
by A2, A4, Th5;
y3 = y39
by A2, A4, Th5;
hence
c1 = c2
by A2, A3, A4, A5, A6, A7, Th5; verum