let n be Nat; :: thesis: - (0* n) = 0* n
set f = 0* n;
set g = - (0* n);
thus len (0* n) = len (- (0* n)) by COMPLSP2:5; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (- (0* n)) or (- (0* n)) . b₁ = (0* n) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (- (0* n)) or (- (0* n)) . k = (0* n) . k )
assume ( 1 <= k & k <= len (- (0* n)) ) ; :: thesis: (- (0* n)) . k = (0* n) . k
A1: (0* n) . k = 0 ;
thus (0* n) . k = - Q
.= (- (0* n)) . k by A1, VALUED_1:8 ; :: thesis: verum