let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i, a1, b1, c1, d1, e1, f1, g1, h1, i1 being Element of K st <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> = <*<*a1,b1,c1*>,<*d1,e1,f1*>,<*g1,h1,i1*>*> holds
( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 )
let a, b, c, d, e, f, g, h, i, a1, b1, c1, d1, e1, f1, g1, h1, i1 be Element of K; :: thesis: ( <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> = <*<*a1,b1,c1*>,<*d1,e1,f1*>,<*g1,h1,i1*>*> implies ( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 ) )
assume <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> = <*<*a1,b1,c1*>,<*d1,e1,f1*>,<*g1,h1,i1*>*> ; :: thesis: ( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 )
then ( <*a,b,c*> = <*a1,b1,c1*> & <*d,e,f*> = <*d1,e1,f1*> & <*g,h,i*> = <*g1,h1,i1*> ) by FINSEQ_1:78;
hence ( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 ) by FINSEQ_1:78; :: thesis: verum