let R be Ring; :: thesis: for X being set holds FS_Funcs (X,R) is LeftMod of R
let X be set ; :: thesis: FS_Funcs (X,R) is LeftMod of R
set V1 = fs_Funcs (X,R);
A1: FS_Funcs (X,R) is Abelian

proof

let v, w be Element of (FS_Funcs (X,R)); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
( v in fs_Funcs (X,R) & w in fs_Funcs (X,R) ) ;
then reconsider v1 = v, w1 = w as Element of Funcs (X, the carrier of R) ;
[v,w] in [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):] ;
then A2: [v,w] in dom ((ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):]) by FUNCT_2:def 1;
[w,v] in [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):] ;
then A3: [w,v] in dom ((ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):]) by FUNCT_2:def 1;
v + w = (ADD (X,R)) . (v1,w1) by A2, FUNCT_1:47
.= (ADD (X,R)) . (w1,v1) by Lm2
.= w + v by A3, FUNCT_1:47 ;
hence v + w = w + v ; :: thesis: verum

end;

A4: FS_Funcs (X,R) is add-associative

proof

let f, g, h be Element of (FS_Funcs (X,R)); :: according to RLVECT_1:def 3 :: thesis: (f + g) + h = f + (g + h)
( f in fs_Funcs (X,R) & g in fs_Funcs (X,R) & h in fs_Funcs (X,R) ) ;
then reconsider f1 = f, g1 = g, h1 = h as Element of Funcs (X, the carrier of R) ;
A5: g + h = (ADD (X,R)) . (g1,h1) by Th5;
f + g = (ADD (X,R)) . (f1,g1) by Th5;
then (f + g) + h = (ADD (X,R)) . (((ADD (X,R)) . (f1,g1)),h1) by Th5
.= (ADD (X,R)) . (f1,((ADD (X,R)) . (g1,h1))) by Lm3
.= f + (g + h) by A5, Th5 ;
hence (f + g) + h = f + (g + h) ; :: thesis: verum

end;

A6: FS_Funcs (X,R) is right_zeroed

proof

let f be Element of (FS_Funcs (X,R)); :: according to RLVECT_1:def 4 :: thesis: f + (0. (FS_Funcs (X,R))) = f
reconsider f1 = f as Element of Funcs (X, the carrier of R) by TARSKI:def 3;
f + (0. (FS_Funcs (X,R))) = (ADD (X,R)) . (f1,(0_Funcs (X,R))) by Th5
.= f1 by Lm13 ;
hence f + (0. (FS_Funcs (X,R))) = f ; :: thesis: verum

end;

A7: FS_Funcs (X,R) is right_complementable

proof

let f be Element of (FS_Funcs (X,R)); :: according to ALGSTR_0:def 16 :: thesis: f is right_complementable
reconsider f1 = f as Element of Funcs (X, the carrier of R) by TARSKI:def 3;
reconsider r = - (1. R) as Element of R ;
r * f = (LMULT (X,R)) . (r,f1) by Lm15;
then f + (r * f) = (ADD (X,R)) . (f1,((LMULT (X,R)) . (r,f1))) by Th5
.= 0. (FS_Funcs (X,R)) by Lm14 ;
hence f is right_complementable ; :: thesis: verum

end;

A8: FS_Funcs (X,R) is vector-distributive

proof

let a be Element of R; :: according to VECTSP_1:def 13 :: thesis: for b₁, b₂ being Element of the carrier of (FS_Funcs (X,R)) holds a * (b₁ + b₂) = (a * b₁) + (a * b₂)
let v, w be Element of (FS_Funcs (X,R)); :: thesis: a * (v + w) = (a * v) + (a * w)
( v in FS_Funcs (X,R) & w in FS_Funcs (X,R) ) ;
then reconsider v1 = v, w1 = w as Element of Funcs (X, the carrier of R) ;
A9: v + w = (ADD (X,R)) . (v1,w1) by Th5;
A10: ( a * v = (LMULT (X,R)) . (a,v1) & a * w = (LMULT (X,R)) . (a,w1) ) by Lm15;
a * (v + w) = (LMULT (X,R)) . (a,((ADD (X,R)) . (v1,w1))) by A9, Lm15
.= (ADD (X,R)) . (((LMULT (X,R)) . (a,v1)),((LMULT (X,R)) . (a,w1))) by Lm4
.= (a * v) + (a * w) by A10, Th5 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

A11: FS_Funcs (X,R) is scalar-distributive

proof

let a, b be Element of R; :: according to VECTSP_1:def 14 :: thesis: for b₁ being Element of the carrier of (FS_Funcs (X,R)) holds (a + b) * b₁ = (a * b₁) + (b * b₁)
let f be Element of (FS_Funcs (X,R)); :: thesis: (a + b) * f = (a * f) + (b * f)
f in FS_Funcs (X,R) ;
then reconsider f1 = f as Element of Funcs (X, the carrier of R) ;
A12: ( a * f = (LMULT (X,R)) . (a,f1) & b * f = (LMULT (X,R)) . (b,f1) ) by Lm15;
(a + b) * f = (LMULT (X,R)) . ((a + b),f1) by Lm15
.= (ADD (X,R)) . (((LMULT (X,R)) . (a,f1)),((LMULT (X,R)) . (b,f1))) by Lm5
.= (a * f) + (b * f) by A12, Th5 ;
hence (a + b) * f = (a * f) + (b * f) ; :: thesis: verum

end;

A13: FS_Funcs (X,R) is scalar-associative

proof

let a, b be Element of R; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of (FS_Funcs (X,R)) holds (a * b) * b₁ = a * (b * b₁)
let f be Element of (FS_Funcs (X,R)); :: thesis: (a * b) * f = a * (b * f)
f in FS_Funcs (X,R) ;
then reconsider f1 = f as Element of Funcs (X, the carrier of R) ;
A14: ( (a * b) * f = (LMULT (X,R)) . ((a * b),f1) & b * f = (LMULT (X,R)) . (b,f1) ) by Lm15;
(a * b) * f = (LMULT (X,R)) . ((a * b),f1) by Lm15
.= (LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f))) by Lm6
.= a * (b * f) by A14, Lm15 ;
hence (a * b) * f = a * (b * f) ; :: thesis: verum

end;

FS_Funcs (X,R) is scalar-unital

proof

let f be Element of (FS_Funcs (X,R)); :: according to VECTSP_1:def 16 :: thesis: (1. R) * f = f
f in FS_Funcs (X,R) ;
then reconsider f1 = f as Element of Funcs (X, the carrier of R) ;
(1. R) * f = (LMULT (X,R)) . ((1. R),f1) by Lm15
.= f by Lm7 ;
hence (1. R) * f = f ; :: thesis: verum

end;

hence FS_Funcs (X,R) is LeftMod of R by A1, A4, A6, A7, A8, A11, A13; :: thesis: verum