let F, G be Function; :: thesis: ( dom F = product f & ( for y being Function st y in dom F holds
F . y = y . x ) & dom G = product f & ( for y being Function st y in dom G holds
G . y = y . x ) implies F = G )
assume that
A3: dom F = product f and
A4: for y being Function st y in dom F holds
F . y = y . x and
A5: dom G = product f and
A6: for y being Function st y in dom G holds
G . y = y . x ; :: thesis: F = G

now :: thesis: for y being object st y in product f holds
F . y = G . y

let y be object ; :: thesis: ( y in product f implies F . y = G . y )
assume A7: y in product f ; :: thesis: F . y = G . y
then reconsider x1 = y as Function ;
thus F . y = x1 . x by A3, A4, A7
.= G . y by A5, A6, A7 ; :: thesis: verum

end;

hence F = G by A3, A5; :: thesis: verum