let F be Field; :: thesis: for a, b, c, f, g, h being Element of F holds [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
let a, b, c, f, g, h be Element of F; :: thesis: [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
set abc = [a,b,c];
set fgh = [f,g,h];
A1: ( [a,b,c] `3_3 = c & [f,g,h] `1_3 = f ) ;
A2: ( [f,g,h] `2_3 = g & [f,g,h] `3_3 = h ) ;
( [a,b,c] `1_3 = a & [a,b,c] `2_3 = b ) ;
hence [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)] by A1, A2, Def1; :: thesis: verum