let f1, f2 be SetSequence of (REAL 1); :: thesis: ( ( 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).]*> ; :: thesis: 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

proof

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then ( g1 . x = product <*[.(a . x),(b . x).]*> & g2 . x = product <*[.(a . x),(b . x).]*> ) by A14, A16;
hence g1 . x = g2 . x ; :: thesis: verum

end;

hence f1 = f2 by A13, A15, A17; :: thesis: verum