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

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)

hence
f = g
; :: thesis: verumfor 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;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