let f1, f2 be SetSequence of (REAL 1); :: thesis: ( ex f being Function of NAT,(bool (REAL 1)) st
( f1 = f & ( for i being Nat holds f . i = product <*[.(a . i),(b . i).]*> ) ) & ex f being Function of NAT,(bool (REAL 1)) st
( f2 = f & ( for i being Nat holds f . i = product <*[.(a . i),(b . i).]*> ) ) implies f1 = f2 )
assume that
A11: ex g1 being Function of NAT,(bool (REAL 1)) st
( f1 = g1 & ( for i being Nat holds g1 . i = product <*[.(a . i),(b . i).]*> ) ) and
A12: ex g2 being Function of NAT,(bool (REAL 1)) st
( f2 = g2 & ( for i being Nat holds g2 . 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