let E, F be RealNormSpace; :: thesis: for s being Point of (product <*E,F*>)
for i being Element of dom <*E,F*>
for x1 being object holds len (s +* (i,x1)) = 2
let s be Point of (product <*E,F*>); :: thesis: for i being Element of dom <*E,F*>
for x1 being object holds len (s +* (i,x1)) = 2
let i be Element of dom <*E,F*>; :: thesis: for x1 being object holds len (s +* (i,x1)) = 2
let x1 be object ; :: thesis: len (s +* (i,x1)) = 2
consider x being Point of E, y being Point of F such that
A3: s = <*x,y*> by PRVECT_3:19;
A1: len s = 2 by FINSEQ_1:44, A3;
dom (s +* (i,x1)) = dom s by FUNCT_7:30
.= Seg 2 by A1, FINSEQ_1:def 3 ;
hence len (s +* (i,x1)) = 2 by FINSEQ_1:def 3; :: thesis: verum