let f1, f2 be SetSequence of (REAL 1); ( ( for i being Nat holds f1 . i = product <*[.(a . i),(b . i).]*> ) & ( for i being Nat holds f2 . i = product <*[.(a . i),(b . i).]*> ) implies f1 = f2 )
assume that
A11:
for i being Nat holds f1 . i = product <*[.(a . i),(b . i).]*>
and
A12:
for i being Nat holds f2 . i = product <*[.(a . i),(b . i).]*>
; f1 = f2
consider g1 being Function of NAT,(bool (REAL 1)) such that
A13:
g1 = f1
and
A14:
for i being Nat holds g1 . i = product <*[.(a . i),(b . i).]*>
by A11;
consider g2 being Function of NAT,(bool (REAL 1)) such that
A15:
g2 = f2
and
A16:
for i being Nat holds g2 . i = product <*[.(a . i),(b . i).]*>
by A12;
A17:
( dom g1 = NAT & dom g2 = NAT )
by FUNCT_2:def 1;
for x being object st x in dom g1 holds
g1 . x = g2 . x
hence
f1 = f2
by A13, A15, A17; verum