let F, G be FinSequence of REAL ; :: thesis: ( dom F = dom G & ( for i being Element of dom F holds G . i = (F . i) " ) implies Product G = (Product F) " )
assume that
A1: dom F = dom G and
A2: for i being Element of dom F holds G . i = (F . i) " ; :: thesis: Product G = (Product F) "
A3: len F = len G by A1, FINSEQ_3:29;
for i being Element of NAT st i in dom F holds
G . i = (F . i) " by A2;
hence Product G = (Product F) " by A3, LM36A; :: thesis: verum