let R be Ring; :: thesis: for X being set
for a being Element of R
for f1 being Element of Funcs (X, the carrier of R)
for f being Element of (FS_Funcs (X,R)) st f1 = f holds
a * f = (LMULT (X,R)) . (a,f1)
let X be set ; :: thesis: for a being Element of R
for f1 being Element of Funcs (X, the carrier of R)
for f being Element of (FS_Funcs (X,R)) st f1 = f holds
a * f = (LMULT (X,R)) . (a,f1)
let a be Element of R; :: thesis: for f1 being Element of Funcs (X, the carrier of R)
for f being Element of (FS_Funcs (X,R)) st f1 = f holds
a * f = (LMULT (X,R)) . (a,f1)
let f1 be Element of Funcs (X, the carrier of R); :: thesis: for f being Element of (FS_Funcs (X,R)) st f1 = f holds
a * f = (LMULT (X,R)) . (a,f1)
let f be Element of (FS_Funcs (X,R)); :: thesis: ( f1 = f implies a * f = (LMULT (X,R)) . (a,f1) )
set V1 = fs_Funcs (X,R);
set CR = the carrier of R;
assume A1: f1 = f ; :: thesis: a * f = (LMULT (X,R)) . (a,f1)
[a,f] in [: the carrier of R,(fs_Funcs (X,R)):] ;
hence a * f = (LMULT (X,R)) . (a,f1) by A1, FUNCT_1:49; :: thesis: verum