thus Base_FinSeq (1,1) =
Replace (<*(In (0,REAL))*>,1,(In (1,REAL)))
by FINSEQ_2:59
.=
<*1*>
by FINSEQ_7:12
; ( Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (2,1) =
Replace (<*(In (0,REAL)),(In (0,REAL))*>,1,(In (1,REAL)))
by FINSEQ_2:61
.=
<*1,0*>
by FINSEQ_7:13
; ( Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (2,2) =
Replace (<*(In (0,REAL)),(In (0,REAL))*>,2,(In (1,REAL)))
by FINSEQ_2:61
.=
<*0,1*>
by FINSEQ_7:14
; ( Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (3,1) =
Replace (<*0,0,0*>,1,(In (1,REAL)))
by FINSEQ_2:62
.=
<*1,0,0*>
by FINSEQ_7:15
; ( Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (3,2) =
Replace (<*(In (0,REAL)),(In (0,REAL)),(In (0,REAL))*>,2,(In (1,REAL)))
by FINSEQ_2:62
.=
<*0,1,0*>
by FINSEQ_7:16
; Base_FinSeq (3,3) = <*0,0,1*>
thus Base_FinSeq (3,3) =
Replace (<*(In (0,REAL)),(In (0,REAL)),(In (0,REAL))*>,3,(In (1,REAL)))
by FINSEQ_2:62
.=
<*0,0,1*>
by FINSEQ_7:17
; verum