let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds seq = seq + (0. X)
let seq be sequence of X; :: thesis: seq = seq + (0. X)

now :: thesis: for n being Element of NAT holds (seq + H₁(X)) . n = seq . n

let n be Element of NAT ; :: thesis: (seq + H₁(X)) . n = seq . n
thus (seq + H₁(X)) . n = (seq . n) + H₁(X) by BHSP_1:def 6
.= seq . n by RLVECT_1:4 ; :: thesis: verum

end;

hence seq = seq + (0. X) by FUNCT_2:63; :: thesis: verum