let it1, it2 be Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)); :: thesis: ( ( for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ) implies it1 = it2 )

assume that

A3: for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) and

A4: for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ; :: thesis: it1 = it2

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ) implies it1 = it2 )

assume that

A3: for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) and

A4: for c being Complex

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ; :: thesis: it1 = it2

now :: thesis: for c being Element of COMPLEX

for f being Element of Funcs (X, the carrier of Y) holds it1 . (c,f) = it2 . (c,f)

hence
it1 = it2
; :: thesis: verumfor f being Element of Funcs (X, the carrier of Y) holds it1 . (c,f) = it2 . (c,f)

let c be Element of COMPLEX ; :: thesis: for f being Element of Funcs (X, the carrier of Y) holds it1 . (c,f) = it2 . (c,f)

let f be Element of Funcs (X, the carrier of Y); :: thesis: it1 . (c,f) = it2 . (c,f)

end;let f be Element of Funcs (X, the carrier of Y); :: thesis: it1 . (c,f) = it2 . (c,f)

now :: thesis: for x being Element of X holds (it1 . [c,f]) . x = (it2 . [c,f]) . x

hence
it1 . (c,f) = it2 . (c,f)
by FUNCT_2:63; :: thesis: verumlet x be Element of X; :: thesis: (it1 . [c,f]) . x = (it2 . [c,f]) . x

thus (it1 . [c,f]) . x = c * (f . x) by A3

.= (it2 . [c,f]) . x by A4 ; :: thesis: verum

end;thus (it1 . [c,f]) . x = c * (f . x) by A3

.= (it2 . [c,f]) . x by A4 ; :: thesis: verum