set cR = center R;
set ccR = the carrier of (center R);
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
set lm = the multF of R | [:the carrier of (center R),the carrier of (centralizer s):];
A1: the carrier of (center R) c= the carrier of R by Th17;
A2: the carrier of (centralizer s) c= the carrier of R by Th24;
A3: dom the multF of R = [:the carrier of R,the carrier of R:] by FUNCT_2:def 1;
[:the carrier of (center R),the carrier of (centralizer s):] c= [:the carrier of R,the carrier of R:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:the carrier of (center R),the carrier of (centralizer s):] or x in [:the carrier of R,the carrier of R:] )
assume x in [:the carrier of (center R),the carrier of (centralizer s):] ; :: thesis: x in [:the carrier of R,the carrier of R:]
then ex x1, x2 being set st
( x1 in the carrier of (center R) & x2 in the carrier of (centralizer s) & x = [x1,x2] ) by ZFMISC_1:def 2;
hence x in [:the carrier of R,the carrier of R:] by A1, A2, ZFMISC_1:def 2; :: thesis: verum

end;

then A4: dom (the multF of R | [:the carrier of (center R),the carrier of (centralizer s):]) = [:the carrier of (center R),the carrier of (centralizer s):] by A3, RELAT_1:91;

now

let x be set ; :: thesis: ( x in [:the carrier of (center R),the carrier of (centralizer s):] implies (the multF of R | [:the carrier of (center R),the carrier of (centralizer s):]) . x in the carrier of (centralizer s) )
assume A5: x in [:the carrier of (center R),the carrier of (centralizer s):] ; :: thesis: (the multF of R | [:the carrier of (center R),the carrier of (centralizer s):]) . x in the carrier of (centralizer s)
then consider x1, x2 being set such that
A6: x1 in the carrier of (center R) and
A7: x2 in the carrier of (centralizer s) and
A8: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of R by A1, A6;
reconsider x2 = x2 as Element of R by A2, A7;
(the multF of R | [:the carrier of (center R),the carrier of (centralizer s):]) . x = x1 * x2 by A5, A8, FUNCT_1:72;
hence (the multF of R | [:the carrier of (center R),the carrier of (centralizer s):]) . x in the carrier of (centralizer s) by A6, A7, Th27; :: thesis: verum

end;

then reconsider lm = the multF of R | [:the carrier of (center R),the carrier of (centralizer s):] as Function of [:the carrier of (center R),the carrier of (centralizer s):],the carrier of (centralizer s) by A4, FUNCT_2:5;
set Vos = VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #);
set cV = the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #);
set aV = the addF of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #);
A9: VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) is VectSp-like

proof

let x, y be Element of the carrier of (center R); :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. (center R)) * b₁ = b₁ )
let v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
A10: x in the carrier of (center R) ;
y in the carrier of (center R) ;
then reconsider xx = x, yy = y as Element of R by A1, A10;
A11: v in the carrier of (centralizer s) ;
w in the carrier of (centralizer s) ;
then reconsider vv = v, ww = w as Element of R by A2, A11;
A12: the multF of (center R) = the multF of R || the carrier of (center R) by Def4;
A13: the addF of (center R) = the addF of R || the carrier of (center R) by Def4;
A14: the addF of (centralizer s) = the addF of R || the carrier of (centralizer s) by Def5;
A15: [x,w] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A16: [x,(v + w)] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A17: [v,w] in [:the carrier of (centralizer s),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A18: [y,v] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A19: [x,v] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A20: [(x + y),v] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A21: [x,(y * v)] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A22: [y,v] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A23: [(x * y),v] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A24: [x,y] in [:the carrier of (center R),the carrier of (center R):] by ZFMISC_1:def 2;
A25: [(x * v),(x * w)] in [:the carrier of (centralizer s),the carrier of (centralizer s):] by ZFMISC_1:def 2;
A26: [(x * v),(y * v)] in [:the carrier of (centralizer s),the carrier of (centralizer s):] by ZFMISC_1:def 2;
thus x * (v + w) = the multF of R . [x,(the addF of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) . [v,w])] by A16, FUNCT_1:72
.= xx * (vv + ww) by A14, A17, FUNCT_1:72
.= (xx * vv) + (xx * ww) by VECTSP_1:def 11
.= the addF of R . [(x * v),(the multF of R . [xx,ww])] by A19, FUNCT_1:72
.= the addF of R . [(x * v),(x * w)] by A15, FUNCT_1:72
.= (x * v) + (x * w) by A14, A25, FUNCT_1:72 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
thus (x + y) * v = the multF of R . [(the addF of (center R) . [x,y]),vv] by A20, FUNCT_1:72
.= (xx + yy) * vv by A13, A24, FUNCT_1:72
.= (xx * vv) + (yy * vv) by VECTSP_1:def 12
.= the addF of R . [(x * v),(the multF of R . [yy,vv])] by A19, FUNCT_1:72
.= the addF of R . [(x * v),(lm . y,v)] by A18, FUNCT_1:72
.= (x * v) + (y * v) by A14, A26, FUNCT_1:72 ; :: thesis: ( (x * y) * v = x * (y * v) & (1. (center R)) * v = v )
thus (x * y) * v = the multF of R . [(the multF of (center R) . x,y),vv] by A23, FUNCT_1:72
.= (xx * yy) * vv by A12, A24, FUNCT_1:72
.= xx * (yy * vv) by GROUP_1:def 4
.= the multF of R . [xx,(lm . y,v)] by A22, FUNCT_1:72
.= x * (y * v) by A21, FUNCT_1:72 ; :: thesis: (1. (center R)) * v = v
1_ R in center R by Th20;
then 1_ R in the carrier of (center R) by STRUCT_0:def 5;
then A27: [(1_ R),vv] in [:the carrier of (center R),the carrier of (centralizer s):] by ZFMISC_1:def 2;
thus (1. (center R)) * v = lm . (1. R),vv by Def4
.= (1. R) * vv by A27, FUNCT_1:72
.= v by VECTSP_1:def 19 ; :: thesis: verum

end;

A28: VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) is add-associative

proof

let u, v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def 6 :: thesis: (u + v) + w = u + (v + w)
reconsider uu = u, vv = v, ww = w as Element of the carrier of (centralizer s) ;
thus (u + v) + w = (uu + vv) + ww
.= uu + (vv + ww) by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

A29: VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) is right_zeroed

proof

let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def 7 :: thesis: v + (0. VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #)) = v
reconsider vv = v as Element of the carrier of (centralizer s) ;
thus v + (0. VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #)) = vv + (0. (centralizer s))
.= v by RLVECT_1:def 7 ; :: thesis: verum

end;

A30: VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) is right_complementable

proof

let v be Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider vv = v as Element of the carrier of (centralizer s) ;
consider ww being Element of the carrier of (centralizer s) such that
A31: vv + ww = 0. (centralizer s) by ALGSTR_0:def 11;
reconsider w = ww as Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) ;
v + w = 0. VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) by A31;
hence ex w being Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) st v + w = 0. VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) ; :: according to ALGSTR_0:def 11 :: thesis: verum

end;

VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #) is Abelian

proof

let v, w be Element of the carrier of VectSpStr(# the carrier of (centralizer s),the addF of (centralizer s),(0. (centralizer s)),lm #); :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
reconsider vv = v, ww = w as Element of the carrier of (centralizer s) ;
thus v + w = ww + vv by RLVECT_1:5
.= w + v ; :: thesis: verum

end;

hence ex b₁ being strict VectSp of center R st
( addLoopStr(# the carrier of b₁,the addF of b₁,the ZeroF of b₁ #) = addLoopStr(# the carrier of (centralizer s),the addF of (centralizer s),the ZeroF of (centralizer s) #) & the lmult of b₁ = the multF of R | [:the carrier of (center R),the carrier of (centralizer s):] ) by A9, A28, A29, A30; :: thesis: verum