let a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 be Real; :: thesis: ( symmetric_3 (a1,a2,a3,a4,a5,a6) = symmetric_3 (b1,b2,b3,b4,b5,b6) implies ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 ) )
assume A1: symmetric_3 (a1,a2,a3,a4,a5,a6) = symmetric_3 (b1,b2,b3,b4,b5,b6) ; :: thesis: ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 )
reconsider fa1 = a1, fa2 = a2, fa3 = a3, fa4 = a4, fa5 = a5, fa6 = a6, fb1 = b1, fb2 = b2, fb3 = b3, fb4 = b4, fb5 = b5, fb6 = b6 as Element of F_Real by XREAL_0:def 1;
<*<*fa1,fa4,fa5*>,<*fa4,fa2,fa6*>,<*fa5,fa6,fa3*>*> = <*<*fb1,fb4,fb5*>,<*fb4,fb2,fb6*>,<*fb5,fb6,fb3*>*> by A1;
hence ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 ) by Th02; :: thesis: verum