let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for F being FinSequence of V
for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2
let F be FinSequence of V; :: thesis: for v1, v2 being Element of V st len F = 2 & v1 = F . 1 & v2 = F . 2 holds
Sum F = v1 + v2
let v1, v2 be Element of V; :: thesis: ( len F = 2 & v1 = F . 1 & v2 = F . 2 implies Sum F = v1 + v2 )
assume ( len F = 2 & v1 = F . 1 & v2 = F . 2 ) ; :: thesis: Sum F = v1 + v2
then F = <*v1,v2*> by FINSEQ_1:44;
hence Sum F = v1 + v2 by Th45; :: thesis: verum