let K be Real; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let s be Element of REAL n; :: thesis:
assume A1: for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . s).| <= K ; :: thesis:
reconsider t = s as Element of (REAL-NS n) by REAL_NS1:def 4;
for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . t).|| <= K

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= n ) ; :: thesis:
then |.((proj (i,n)) . t).| <= K by A1;
hence ||.((Proj (i,n)) . t).|| <= K by Th4; :: thesis:

end;