let x, y be Real; :: thesis: for x1, x2, x3 being real-valued FinSequence 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 real-valued FinSequence; :: thesis: ( len x1 = len x2 & len x2 = len x3 implies |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) )
assume that
A1: len x1 = len x2 and
A2: len x2 = len x3 ; :: thesis: |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
( len (x * x1) = len x1 & len (y * x2) = len x2 ) by Th117;
then |(((x * x1) + (y * x2)),x3)| = |((x * x1),x3)| + |((y * x2),x3)| by A1, A2, Th120
.= (x * |(x1,x3)|) + |((y * x2),x3)| by A1, A2, Th121
.= (x * |(x1,x3)|) + (y * |(x2,x3)|) by A2, Th121 ;
hence |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ; :: thesis: verum