let X be RealUnitarySpace; :: thesis: for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
let seq1, seq2, seq3 be sequence of X; :: thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (seq1 - (seq2 + seq3)) . n = ((seq1 - seq2) - seq3) . n
thus (seq1 - (seq2 + seq3)) . n = (seq1 . n) - ((seq2 + seq3) . n) by NORMSP_1:def 3
.= (seq1 . n) - ((seq2 . n) + (seq3 . n)) by NORMSP_1:def 2
.= ((seq1 . n) - (seq2 . n)) - (seq3 . n) by RLVECT_1:27
.= ((seq1 - seq2) . n) - (seq3 . n) by NORMSP_1:def 3
.= ((seq1 - seq2) - seq3) . n by NORMSP_1:def 3 ; :: thesis: verum