let f, g be Function of [:the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F); :: thesis: ( ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . x,v = the multF of F [;] x,v ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds g . x,v = the multF of F [;] x,v ) implies f = g )
assume that
A5: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . x,v = the multF of F [;] x,v and
A6: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds g . x,v = the multF of F [;] x,v ; :: thesis: f = g

now

let x be Element of F; :: thesis: for v being Element of n -tuples_on the carrier of F holds f . x,v = g . x,v
let v be Element of n -tuples_on the carrier of F; :: thesis: f . x,v = g . x,v
f . x,v = the multF of F [;] x,v by A5;
hence f . x,v = g . x,v by A6; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum