let it1, it2 be FinSequence of D; :: thesis: ( dom it1 = dom f & ( for i being Nat st i in dom it1 holds
( ( i in X implies it1 . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies it1 . i = f . i ) ) ) & dom it2 = dom f & ( for i being Nat st i in dom it2 holds
( ( i in X implies it2 . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies it2 . i = f . i ) ) ) implies it1 = it2 )
assume that
A6: dom it1 = dom f and
A7: for i being Nat st i in dom it1 holds
( ( i in X implies it1 . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies it1 . i = f . i ) ) and
A8: dom it2 = dom f and
A9: for i being Nat st i in dom it2 holds
( ( i in X implies it2 . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies it2 . i = f . i ) ) ; :: thesis: it1 = it2
for i being Nat st i in dom it1 holds
it1 . i = it2 . i

proof

let i be Nat; :: thesis: ( i in dom it1 implies it1 . i = it2 . i )
assume A10: i in dom it1 ; :: thesis: it1 . i = it2 . i

per cases ( i in X or not i in X ) ;

suppose A11: i in X ; :: thesis: it1 . i = it2 . i

hence it1 . i = (the_inverseOp_wrt B) . (f . i) by A10, A7
.= it2 . i by A6, A8, A9, A11, A10 ;
:: thesis: verum

end;

suppose A12: not i in X ; :: thesis: it1 . i = it2 . i

hence it1 . i = f . i by A7, A10
.= it2 . i by A9, A6, A8, A12, A10 ;
:: thesis: verum

end;

end;

end;

hence it1 = it2 by A6, A8; :: thesis: verum