let n be Nat; :: thesis: for x1, x2 being Element of REAL n

for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

let x1, x2 be Element of REAL n; :: thesis: for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

let a be Real; :: thesis: |((a * x1),x2)| = a * |(x1,x2)|

( len x1 = n & len x2 = n ) by CARD_1:def 7;

hence |((a * x1),x2)| = a * |(x1,x2)| by RVSUM_1:121; :: thesis: verum

for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

let x1, x2 be Element of REAL n; :: thesis: for a being Real holds |((a * x1),x2)| = a * |(x1,x2)|

let a be Real; :: thesis: |((a * x1),x2)| = a * |(x1,x2)|

( len x1 = n & len x2 = n ) by CARD_1:def 7;

hence |((a * x1),x2)| = a * |(x1,x2)| by RVSUM_1:121; :: thesis: verum