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