thus Base_FinSeq (1,1) = Replace (<*(In (0,REAL))*>,1,(In (1,REAL))) by FINSEQ_2:59
.= <*1*> by FINSEQ_7:12 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum