let D be non empty set ; :: thesis: for M being Matrix of 3,1,D holds
( Line (M,1) = <*(M * (1,1))*> & Line (M,2) = <*(M * (2,1))*> & Line (M,3) = <*(M * (3,1))*> )
let M be Matrix of 3,1,D; :: thesis: ( Line (M,1) = <*(M * (1,1))*> & Line (M,2) = <*(M * (2,1))*> & Line (M,3) = <*(M * (3,1))*> )
A1: ( len M = 3 & width M = 1 & Indices M = [:(Seg 3),(Seg 1):] ) by MATRIX_0:23;
now :: thesis: ( dom (Line (M,1)) = dom <*(M * (1,1))*> & ( for x being object st x in dom (Line (M,1)) holds
(Line (M,1)) . x = <*(M * (1,1))*> . x ) )
A2: len (Line (M,1)) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23 ;
dom <*(M * (1,1))*> = Seg 1 by FINSEQ_1:def 8;
hence dom (Line (M,1)) = dom <*(M * (1,1))*> by A2, FINSEQ_1:def 3; :: thesis: for x being object st x in dom (Line (M,1)) holds
(Line (M,1)) . x = <*(M * (1,1))*> . x
thus for x being object st x in dom (Line (M,1)) holds
(Line (M,1)) . x = <*(M * (1,1))*> . x :: thesis: verum
proof
let x be object ; :: thesis: ( x in dom (Line (M,1)) implies (Line (M,1)) . x = <*(M * (1,1))*> . x )
assume x in dom (Line (M,1)) ; :: thesis: (Line (M,1)) . x = <*(M * (1,1))*> . x
then x in {1} by A2, FINSEQ_1:def 3, FINSEQ_1:2;
then A3: x = 1 by TARSKI:def 1;
(Line (M,1)) . 1 = M * (1,1) by A1, FINSEQ_1:1, MATRIX_0:def 7
.= <*(M * (1,1))*> . 1 by FINSEQ_1:def 8 ;
hence (Line (M,1)) . x = <*(M * (1,1))*> . x by A3; :: thesis: verum
end;
end;
hence Line (M,1) = <*(M * (1,1))*> by FUNCT_1:def 11; :: thesis: ( Line (M,2) = <*(M * (2,1))*> & Line (M,3) = <*(M * (3,1))*> )
now :: thesis: ( dom (Line (M,2)) = dom <*(M * (2,1))*> & ( for x being object st x in dom (Line (M,2)) holds
(Line (M,2)) . x = <*(M * (2,1))*> . x ) )
A4: len (Line (M,2)) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23 ;
dom <*(M * (2,1))*> = Seg 1 by FINSEQ_1:def 8;
hence dom (Line (M,2)) = dom <*(M * (2,1))*> by A4, FINSEQ_1:def 3; :: thesis: for x being object st x in dom (Line (M,2)) holds
(Line (M,2)) . x = <*(M * (2,1))*> . x
thus for x being object st x in dom (Line (M,2)) holds
(Line (M,2)) . x = <*(M * (2,1))*> . x :: thesis: verum
proof
let x be object ; :: thesis: ( x in dom (Line (M,2)) implies (Line (M,2)) . x = <*(M * (2,1))*> . x )
assume x in dom (Line (M,2)) ; :: thesis: (Line (M,2)) . x = <*(M * (2,1))*> . x
then x in {1} by A4, FINSEQ_1:def 3, FINSEQ_1:2;
then A5: x = 1 by TARSKI:def 1;
(Line (M,2)) . 1 = M * (2,1) by A1, FINSEQ_1:1, MATRIX_0:def 7
.= <*(M * (2,1))*> . 1 by FINSEQ_1:def 8 ;
hence (Line (M,2)) . x = <*(M * (2,1))*> . x by A5; :: thesis: verum
end;
end;
hence Line (M,2) = <*(M * (2,1))*> by FUNCT_1:def 11; :: thesis: Line (M,3) = <*(M * (3,1))*>
now :: thesis: ( dom (Line (M,3)) = dom <*(M * (3,1))*> & ( for x being object st x in dom (Line (M,3)) holds
(Line (M,3)) . x = <*(M * (3,1))*> . x ) )
A6: len (Line (M,3)) = width M by MATRIX_0:def 7
.= 1 by MATRIX_0:23 ;
dom <*(M * (3,1))*> = Seg 1 by FINSEQ_1:def 8;
hence dom (Line (M,3)) = dom <*(M * (3,1))*> by A6, FINSEQ_1:def 3; :: thesis: for x being object st x in dom (Line (M,3)) holds
(Line (M,3)) . x = <*(M * (3,1))*> . x
thus for x being object st x in dom (Line (M,3)) holds
(Line (M,3)) . x = <*(M * (3,1))*> . x :: thesis: verum
proof
let x be object ; :: thesis: ( x in dom (Line (M,3)) implies (Line (M,3)) . x = <*(M * (3,1))*> . x )
assume x in dom (Line (M,3)) ; :: thesis: (Line (M,3)) . x = <*(M * (3,1))*> . x
then x in {1} by A6, FINSEQ_1:def 3, FINSEQ_1:2;
then A7: x = 1 by TARSKI:def 1;
(Line (M,3)) . 1 = M * (3,1) by A1, FINSEQ_1:1, MATRIX_0:def 7
.= <*(M * (3,1))*> . 1 by FINSEQ_1:def 8 ;
hence (Line (M,3)) . x = <*(M * (3,1))*> . x by A7; :: thesis: verum
end;
end;
hence Line (M,3) = <*(M * (3,1))*> by FUNCT_1:def 11; :: thesis: verum