let V be non empty UNITSTR ; :: thesis: for u being Point of V
for x being FinSequence of V
for i being Nat st 1 <= i & i <= len x holds
((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i)
let u be Point of V; :: thesis: for x being FinSequence of V
for i being Nat st 1 <= i & i <= len x holds
((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i)
let x be FinSequence of V; :: thesis: for i being Nat st 1 <= i & i <= len x holds
((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i)
let i be Nat; :: thesis: ( 1 <= i & i <= len x implies ((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i) )
assume A1: ( 1 <= i & i <= len x ) ; :: thesis: ((u .|. x) (*) x) . i = (u .|. (x /. i)) * (x /. i)
len (u .|. x) = len x by DefSK;
then i in dom (u .|. x) by A1, FINSEQ_3:25;
then A2: (u .|. x) . i = (u .|. x) /. i by PARTFUN1:def 6;
thus ((u .|. x) (*) x) . i = ((u .|. x) /. i) * (x /. i) by A1, DefR
.= (u .|. (x /. i)) * (x /. i) by A1, A2, DefSK ; :: thesis: verum