let x, y be real number ; :: thesis: for x1, x2, x3 being FinSequence of REAL st len x1 = len x2 & len x2 = len x3 holds
|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
let x1, x2, x3 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len x2 = len x3 implies |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) )
assume A1: ( len x1 = len x2 & len x2 = len x3 ) ; :: thesis: |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
A2: len (x * x1) = len x1 by Th8;
len (y * x2) = len x2 by Th8;
then |(((x * x1) + (y * x2)),x3)| = |((x * x1),x3)| + |((y * x2),x3)| by A1, A2, Th19
.= (x * |(x1,x3)|) + |((y * x2),x3)| by A1, Th20
.= (x * |(x1,x3)|) + (y * |(x2,x3)|) by A1, Th20 ;
hence |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ; :: thesis: verum