let R be Ring; :: thesis: for X being set
for a being Element of the carrier of R
for f, h being Element of Funcs (X, the carrier of R) holds
( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )
let X be set ; :: thesis: for a being Element of the carrier of R
for f, h being Element of Funcs (X, the carrier of R) holds
( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )
let a be Element of the carrier of R; :: thesis: for f, h being Element of Funcs (X, the carrier of R) holds
( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )
let f, h be Element of Funcs (X, the carrier of R); :: thesis: ( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) )
( ( for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) ) implies h = (LMULT (X,R)) . (a,f) )

proof

assume A1: for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) ; :: thesis: h = (LMULT (X,R)) . (a,f)
B2: ( dom h = X & dom ((LMULT (X,R)) . (a,f)) = X ) by FUNCT_2:92;
for x being object st x in dom h holds
h . x = ((LMULT (X,R)) . (a,f)) . x

proof

let x be object ; :: thesis: ( x in dom h implies h . x = ((LMULT (X,R)) . (a,f)) . x )
assume A2: x in dom h ; :: thesis: h . x = ((LMULT (X,R)) . (a,f)) . x
hence h . x = the multF of R . (a,(f . x)) by A1
.= ((LMULT (X,R)) . (a,f)) . x by A2, Def7 ;
:: thesis: verum

end;

hence h = (LMULT (X,R)) . (a,f) by B2; :: thesis: verum

end;

hence ( h = (LMULT (X,R)) . (a,f) iff for x being object st x in X holds
h . x = the multF of R . (a,(f . x)) ) by Def7; :: thesis: verum