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