let G1, G2 be Go-board; :: thesis: ( len G1 = len G & ( for k being Element of NAT st k in dom G holds
G1 . k = Del ((Line (G,k)),i) ) & len G2 = len G & ( for k being Element of NAT st k in dom G holds
G2 . k = Del ((Line (G,k)),i) ) implies G1 = G2 )
assume that
A79: ( len G1 = len G & ( for k being Element of NAT st k in dom G holds
G1 . k = Del ((Line (G,k)),i) ) ) and
A80: ( len G2 = len G & ( for k being Element of NAT st k in dom G holds
G2 . k = Del ((Line (G,k)),i) ) ) ; :: thesis: G1 = G2
A81: dom G1 = Seg (len G) by A79, FINSEQ_1:def 3;

now

let k be Nat; :: thesis: ( k in dom G1 implies G1 . k = G2 . k )
assume k in dom G1 ; :: thesis: G1 . k = G2 . k
then A82: k in dom G by A81, FINSEQ_1:def 3;
hence G1 . k = Del ((Line (G,k)),i) by A79
.= G2 . k by A80, A82 ;
:: thesis: verum

end;

hence G1 = G2 by A79, A80, FINSEQ_2:9; :: thesis: verum