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 = c & [f,g,h] `1 = f ) by MCART_1:43;
A2: ( [f,g,h] `2 = g & [f,g,h] `3 = h ) by MCART_1:43;
( [a,b,c] `1 = a & [a,b,c] `2 = b ) by MCART_1:43;
hence [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)] by A1, A2, Def1; :: thesis: verum