let it1, it2 be Function of [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):],(Funcs ( the carrier of M, the carrier of N)); :: thesis: ( ( for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (it1 . [a,f]) . x = a * (f . x) ) & ( for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (it2 . [a,f]) . x = a * (f . x) ) implies it1 = it2 )
assume that
A4: for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (it1 . [a,f]) . x = a * (f . x) and
A5: for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (it2 . [a,f]) . x = a * (f . x) ; :: thesis: it1 = it2

now :: thesis: for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds it1 . [a,f] = it2 . [a,f]

let a be Element of the carrier of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N) holds it1 . [a,f] = it2 . [a,f]
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: it1 . [a,f] = it2 . [a,f]

now :: thesis: for x being Element of the carrier of M holds (it1 . [a,f]) . x = (it2 . [a,f]) . x

let x be Element of the carrier of M; :: thesis: (it1 . [a,f]) . x = (it2 . [a,f]) . x
thus (it1 . [a,f]) . x = a * (f . x) by A4
.= (it2 . [a,f]) . x by A5 ; :: thesis: verum

end;

hence it1 . [a,f] = it2 . [a,f] ; :: thesis: verum

end;

hence it1 = it2 ; :: thesis: verum