let D be non empty set ; 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; ( 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 ( 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;
for x being object st x in dom (Line (M,1)) holds
(Line (M,1)) . x = <*(M * (1,1))*> . xthus
for
x being
object st
x in dom (Line (M,1)) holds
(Line (M,1)) . x = <*(M * (1,1))*> . x
verumproof
let x be
object ;
( x in dom (Line (M,1)) implies (Line (M,1)) . x = <*(M * (1,1))*> . x )
assume
x in dom (Line (M,1))
;
(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;
verum
end; end;
hence
Line (M,1) = <*(M * (1,1))*>
by FUNCT_1:def 11; ( Line (M,2) = <*(M * (2,1))*> & Line (M,3) = <*(M * (3,1))*> )
now ( 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;
for x being object st x in dom (Line (M,2)) holds
(Line (M,2)) . x = <*(M * (2,1))*> . xthus
for
x being
object st
x in dom (Line (M,2)) holds
(Line (M,2)) . x = <*(M * (2,1))*> . x
verumproof
let x be
object ;
( x in dom (Line (M,2)) implies (Line (M,2)) . x = <*(M * (2,1))*> . x )
assume
x in dom (Line (M,2))
;
(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;
verum
end; end;
hence
Line (M,2) = <*(M * (2,1))*>
by FUNCT_1:def 11; Line (M,3) = <*(M * (3,1))*>
now ( 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;
for x being object st x in dom (Line (M,3)) holds
(Line (M,3)) . x = <*(M * (3,1))*> . xthus
for
x being
object st
x in dom (Line (M,3)) holds
(Line (M,3)) . x = <*(M * (3,1))*> . x
verumproof
let x be
object ;
( x in dom (Line (M,3)) implies (Line (M,3)) . x = <*(M * (3,1))*> . x )
assume
x in dom (Line (M,3))
;
(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;
verum
end; end;
hence
Line (M,3) = <*(M * (3,1))*>
by FUNCT_1:def 11; verum