set Mx = Mx2Tran M,b1,B2;

per cases ( len b1 = 0 or len b1 > 0 ) ;

suppose A1: len b1 = 0 ; :: thesis: ( Mx2Tran M,b1,B2 is homogeneous & Mx2Tran M,b1,B2 is additive )

A2: now

let a be Scalar of K; :: thesis: for v1 being Vector of V1 holds (Mx2Tran M,b1,B2) . (a * v1) = a * ((Mx2Tran M,b1,B2) . v1)
let v1 be Vector of V1; :: thesis: (Mx2Tran M,b1,B2) . (a * v1) = a * ((Mx2Tran M,b1,B2) . v1)
thus (Mx2Tran M,b1,B2) . (a * v1) = 0. V2 by A1, Th33
.= a * (0. V2) by VECTSP_1:59
.= a * ((Mx2Tran M,b1,B2) . v1) by A1, Th33 ; :: thesis: verum

end;

now

let v1, w1 be Vector of V1; :: thesis: (Mx2Tran M,b1,B2) . (v1 + w1) = ((Mx2Tran M,b1,B2) . v1) + ((Mx2Tran M,b1,B2) . w1)
thus (Mx2Tran M,b1,B2) . (v1 + w1) = 0. V2 by A1, Th33
.= (0. V2) + (0. V2) by RLVECT_1:def 7
.= ((Mx2Tran M,b1,B2) . v1) + (0. V2) by A1, Th33
.= ((Mx2Tran M,b1,B2) . v1) + ((Mx2Tran M,b1,B2) . w1) by A1, Th33 ; :: thesis: verum

end;

then ( Mx2Tran M,b1,B2 is additive & Mx2Tran M,b1,B2 is homogeneous ) by A2, MOD_2:def 3, GRCAT_1:def 13;
hence ( Mx2Tran M,b1,B2 is homogeneous & Mx2Tran M,b1,B2 is additive ) ; :: thesis: verum

end;

suppose A3: len b1 > 0 ; :: thesis: ( Mx2Tran M,b1,B2 is homogeneous & Mx2Tran M,b1,B2 is additive )

A4: now

let v1, w1 be Vector of V1; :: thesis: (Mx2Tran M,b1,B2) . (v1 + w1) = ((Mx2Tran M,b1,B2) . v1) + ((Mx2Tran M,b1,B2) . w1)
set vb = v1 |-- b1;
set wb = w1 |-- b1;
set vwb = (v1 + w1) |-- b1;
set Lvw = LineVec2Mx ((v1 + w1) |-- b1);
set Lv = LineVec2Mx (v1 |-- b1);
set Lw = LineVec2Mx (w1 |-- b1);
set LLvw = Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1;
set LLv = Line ((LineVec2Mx (v1 |-- b1)) * M),1;
set LLw = Line ((LineVec2Mx (w1 |-- b1)) * M),1;
A5: len (LineVec2Mx (w1 |-- b1)) = 1 by MATRIX_1:24;
A6: len b1 = len (v1 |-- b1) by MATRLIN:def 9;
A7: len M = len b1 by A3, MATRIX_1:24;
A8: width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) by MATRIX_1:24;
then A9: width ((LineVec2Mx (v1 |-- b1)) * M) = width M by A7, A6, MATRIX_3:def 4;
then A10: len (Line ((LineVec2Mx (v1 |-- b1)) * M),1) = width M by FINSEQ_1:def 18;
A11: len (LineVec2Mx (v1 |-- b1)) = 1 by MATRIX_1:24;
then A12: len ((LineVec2Mx (v1 |-- b1)) * M) = 1 by A8, A7, A6, MATRIX_3:def 4;
A13: len b1 = len (w1 |-- b1) by MATRLIN:def 9;
( width (LineVec2Mx ((v1 + w1) |-- b1)) = len ((v1 + w1) |-- b1) & len b1 = len ((v1 + w1) |-- b1) ) by MATRIX_1:24, MATRLIN:def 9;
then width ((LineVec2Mx ((v1 + w1) |-- b1)) * M) = width M by A7, MATRIX_3:def 4;
then A14: len (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1) = width M by FINSEQ_1:def 18;
A15: dom (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) = (dom (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)) /\ (dom B2) by Lm1
.= (dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1)) /\ (dom B2) by A14, A10, FINSEQ_3:31
.= dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) by Lm1 ;
A16: width (LineVec2Mx (w1 |-- b1)) = len (w1 |-- b1) by MATRIX_1:24;
then A17: width ((LineVec2Mx (w1 |-- b1)) * M) = width M by A7, A13, MATRIX_3:def 4;
then A18: len (Line ((LineVec2Mx (w1 |-- b1)) * M),1) = width M by FINSEQ_1:def 18;
A19: dom (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) = (dom (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1)) /\ (dom B2) by Lm1
.= (dom (Line ((LineVec2Mx (w1 |-- b1)) * M),1)) /\ (dom B2) by A14, A18, FINSEQ_3:31
.= dom (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) by Lm1 ;
then A20: len (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) = len (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) by FINSEQ_3:31;
LineVec2Mx ((v1 + w1) |-- b1) = LineVec2Mx ((v1 |-- b1) + (w1 |-- b1)) by Th17
.= (LineVec2Mx (v1 |-- b1)) + (LineVec2Mx (w1 |-- b1)) by A6, A13, MATRIX15:27 ;
then (LineVec2Mx ((v1 + w1) |-- b1)) * M = ((LineVec2Mx (v1 |-- b1)) * M) + ((LineVec2Mx (w1 |-- b1)) * M) by A3, A11, A8, A5, A16, A7, A6, A13, MATRIX_4:63;
then Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1 = (Line ((LineVec2Mx (v1 |-- b1)) * M),1) + (Line ((LineVec2Mx (w1 |-- b1)) * M),1) by A12, A9, A17, Lm5;
then A21: lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2 = (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) + (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) by Th7;

A22: now

let i be Element of NAT ; :: thesis: ( i in dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) implies (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) . i = ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i) + ((lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) /. i) )
assume A23: i in dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) ; :: thesis: (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) . i = ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i) + ((lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) /. i)
( (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i = (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) . i & (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) /. i = (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) . i ) by A15, A19, A23, PARTFUN1:def 8;
hence (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) . i = ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i) + ((lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2) /. i) by A21, A15, A23, FVSUM_1:21; :: thesis: verum

end;

len (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) = len (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) by A15, FINSEQ_3:31;
then Sum (lmlt (Line ((LineVec2Mx ((v1 + w1) |-- b1)) * M),1),B2) = (Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2)) + (Sum (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2)) by A20, A22, RLVECT_2:4;
hence (Mx2Tran M,b1,B2) . (v1 + w1) = (Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2)) + (Sum (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2)) by Def3
.= ((Mx2Tran M,b1,B2) . v1) + (Sum (lmlt (Line ((LineVec2Mx (w1 |-- b1)) * M),1),B2)) by Def3
.= ((Mx2Tran M,b1,B2) . v1) + ((Mx2Tran M,b1,B2) . w1) by Def3 ;
:: thesis: verum

end;

now

let a be Scalar of K; :: thesis: for v1 being Vector of V1 holds (Mx2Tran M,b1,B2) . (a * v1) = a * ((Mx2Tran M,b1,B2) . v1)
let v1 be Vector of V1; :: thesis: (Mx2Tran M,b1,B2) . (a * v1) = a * ((Mx2Tran M,b1,B2) . v1)
set vb = v1 |-- b1;
set avb = (a * v1) |-- b1;
set Lav = LineVec2Mx ((a * v1) |-- b1);
set Lv = LineVec2Mx (v1 |-- b1);
set LLav = Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1;
set LLv = Line ((LineVec2Mx (v1 |-- b1)) * M),1;
A24: len M = len b1 by A3, MATRIX_1:24;
( width (LineVec2Mx ((a * v1) |-- b1)) = len ((a * v1) |-- b1) & len b1 = len ((a * v1) |-- b1) ) by MATRIX_1:24, MATRLIN:def 9;
then width ((LineVec2Mx ((a * v1) |-- b1)) * M) = width M by A24, MATRIX_3:def 4;
then A25: len (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) = width M by FINSEQ_1:def 18;
A26: ( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len b1 = len (v1 |-- b1) ) by MATRIX_1:24, MATRLIN:def 9;
then width ((LineVec2Mx (v1 |-- b1)) * M) = width M by A24, MATRIX_3:def 4;
then len (Line ((LineVec2Mx (v1 |-- b1)) * M),1) = width M by FINSEQ_1:def 18;
then A27: dom (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) = dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1) by A25, FINSEQ_3:31;
LineVec2Mx ((a * v1) |-- b1) = LineVec2Mx (a * (v1 |-- b1)) by Th18
.= a * (LineVec2Mx (v1 |-- b1)) by MATRIX15:29 ;
then A28: (LineVec2Mx ((a * v1) |-- b1)) * M = a * ((LineVec2Mx (v1 |-- b1)) * M) by A24, A26, MATRIX15:1;
A29: dom (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) = (dom (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1)) /\ (dom B2) by Lm1;
A30: (dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1)) /\ (dom B2) = dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) by Lm1;
len (LineVec2Mx (v1 |-- b1)) = 1 by MATRIX_1:24;
then len ((LineVec2Mx (v1 |-- b1)) * M) = 1 by A24, A26, MATRIX_3:def 4;
then A31: Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1 = a * (Line ((LineVec2Mx (v1 |-- b1)) * M),1) by A28, MATRIXR1:20;

A32: now

let i be Element of NAT ; :: thesis: ( i in dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) implies (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) . i = a * ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i) )
assume A33: i in dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) ; :: thesis: (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) . i = a * ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i)
A34: (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) . i = (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i by A33, PARTFUN1:def 8;
i in dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1) by A30, A33, XBOOLE_0:def 4;
then A35: (Line ((LineVec2Mx (v1 |-- b1)) * M),1) . i = (Line ((LineVec2Mx (v1 |-- b1)) * M),1) /. i by PARTFUN1:def 8;
i in dom B2 by A30, A33, XBOOLE_0:def 4;
then A36: B2 . i = B2 /. i by PARTFUN1:def 8;
A37: i in dom (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) by A27, A30, A33, XBOOLE_0:def 4;
then A38: (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) . i = (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) /. i by PARTFUN1:def 8;
hence (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) . i = the lmult of V2 . ((Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1) /. i),(B2 /. i) by A29, A27, A30, A33, A36, FUNCOP_1:28
.= (a * ((Line ((LineVec2Mx (v1 |-- b1)) * M),1) /. i)) * (B2 /. i) by A31, A37, A35, A38, FVSUM_1:62
.= a * (((Line ((LineVec2Mx (v1 |-- b1)) * M),1) /. i) * (B2 /. i)) by VECTSP_1:def 28
.= a * ((lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) /. i) by A33, A35, A36, A34, FUNCOP_1:28 ;
:: thesis: verum

end;

len (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) = len (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) by A29, A27, A30, FINSEQ_3:31;
then Sum (lmlt (Line ((LineVec2Mx ((a * v1) |-- b1)) * M),1),B2) = a * (Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2)) by A32, VECTSP_3:10;
hence (Mx2Tran M,b1,B2) . (a * v1) = a * (Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2)) by Def3
.= a * ((Mx2Tran M,b1,B2) . v1) by Def3 ;
:: thesis: verum

end;

then ( Mx2Tran M,b1,B2 is additive & Mx2Tran M,b1,B2 is homogeneous ) by A4, MOD_2:def 3, GRCAT_1:def 13;
hence ( Mx2Tran M,b1,B2 is homogeneous & Mx2Tran M,b1,B2 is additive ) ; :: thesis: verum

end;

end;