thus Base_FinSeq (1,1) = Replace (<*0*>,1,1) by FINSEQ_2:73
.= <*1*> by FINSEQ_7:14 ; :: 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 (<*0,0*>,1,1) by FINSEQ_2:75
.= <*1,0*> by FINSEQ_7:15 ; :: 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 (<*0,0*>,2,1) by FINSEQ_2:75
.= <*0,1*> by FINSEQ_7:16 ; :: 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,1) by FINSEQ_2:76
.= <*1,0,0*> by FINSEQ_7:17 ; :: thesis: ( Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (3,2) = Replace (<*0,0,0*>,2,1) by FINSEQ_2:76
.= <*0,1,0*> by FINSEQ_7:18 ; :: thesis: Base_FinSeq (3,3) = <*0,0,1*>
thus Base_FinSeq (3,3) = Replace (<*0,0,0*>,3,1) by FINSEQ_2:76
.= <*0,0,1*> by FINSEQ_7:19 ; :: thesis: verum