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
A8: 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
A9: 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 :: thesis: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = g . (x,v)
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 A8;
hence f . (x,v) = g . (x,v) by A9; :: thesis: verum
end;
hence f = g ; :: thesis: verum