:: ALGSTR_3 semantic presentation

begin

definition
attr c1 is strict ;
struct TernaryFieldStr -> ( ( ) ( ) ZeroOneStr ) ;
aggr TernaryFieldStr(# carrier, ZeroF, OneF, TernOp #) -> ( ( strict ) ( strict ) TernaryFieldStr ) ;
sel TernOp c1 -> ( ( V25() V34(K8( the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) ( V25() V34(K8( the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) TriOp of the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty for ( ( ) ( ) TernaryFieldStr ) ;
end;

definition
let F be ( ( non empty ) ( non empty ) TernaryFieldStr ) ;
mode Scalar of F is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let F be ( ( non empty ) ( non empty ) TernaryFieldStr ) ;
let a, b, c be ( ( ) ( ) Scalar of F : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ;
func Tern (a,b,c) -> ( ( ) ( ) Scalar of F : ( ( ) ( ) 2-sorted ) ) equals :: ALGSTR_3:def 1
 the TernOp of F : ( ( ) ( ) 2-sorted ) : ( ( V25() V34(K8( the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) ( V25() V34(K8( the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) TriOp of the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) . (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of F : ( ( ) ( ) 2-sorted ) ) ,c : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
func ternaryreal -> ( ( V25() V34(K8(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ) ( V25() V34(K8(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ) TriOp of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) means :: ALGSTR_3:def 2
 for a, b, c being ( ( ) ( V11() V12() ) Real) holds it : ( ( ) ( ) 2-sorted ) . (a : ( ( ) ( V11() V12() ) Real) ,b : ( ( ) ( V11() V12() ) Real) ,c : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) = (a : ( ( ) ( V11() V12() ) Real) * b : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) + c : ( ( ) ( V11() V12() ) Real) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ;
end;

definition
func TernaryFieldEx -> ( ( strict ) ( strict ) TernaryFieldStr ) equals :: ALGSTR_3:def 3
 TernaryFieldStr(# REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,0 : ( ( ) ( V10() V11() V12() V13() V14() V15() V16() V17() V18() ) Element of NAT : ( ( ) ( V13() V14() V15() V16() V17() V18() V19() ) Element of K6(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V10() V11() V12() V13() V14() V15() V16() V17() V18() ) Element of NAT : ( ( ) ( V13() V14() V15() V16() V17() V18() V19() ) Element of K6(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) ) ) ,ternaryreal : ( ( V25() V34(K8(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ) ( V25() V34(K8(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ) TriOp of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) #) : ( ( strict ) ( strict ) TernaryFieldStr ) ;
end;

registration
cluster TernaryFieldEx : ( ( strict ) ( strict ) TernaryFieldStr ) -> non empty strict ;
end;

definition
let a, b, c be ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) ;
func tern (a,b,c) -> ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) equals :: ALGSTR_3:def 4
 the TernOp of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( V25() V34(K8( the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) ) ( V25() V34(K8( the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) ) TriOp of the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) . (a : ( ( V42() ) ( V42() ) set ) ,b : ( ( ) ( ) set ) ,c : ( ( ) ( ) Element of a : ( ( V42() ) ( V42() ) set ) ) ) : ( ( ) ( ) Element of the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: ALGSTR_3:1
for u, u9, v, v9 being ( ( ) ( V11() V12() ) Real) st u : ( ( ) ( V11() V12() ) Real) <> u9 : ( ( ) ( V11() V12() ) Real) holds
ex x being ( ( ) ( V11() V12() ) Real) st (u : ( ( ) ( V11() V12() ) Real) * x : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) + v : ( ( ) ( V11() V12() ) Real) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) = (u9 : ( ( ) ( V11() V12() ) Real) * x : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) + v9 : ( ( ) ( V11() V12() ) Real) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ;

theorem :: ALGSTR_3:2
for u, a, v being ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) )
for z, x, y being ( ( ) ( V11() V12() ) Real) st u : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) = z : ( ( ) ( V11() V12() ) Real) & a : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) = x : ( ( ) ( V11() V12() ) Real) & v : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) = y : ( ( ) ( V11() V12() ) Real) holds
Tern (u : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) ) = (z : ( ( ) ( V11() V12() ) Real) * x : ( ( ) ( V11() V12() ) Real) ) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) + y : ( ( ) ( V11() V12() ) Real) : ( ( ) ( V11() V12() ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) ;

theorem :: ALGSTR_3:3
1 : ( ( ) ( non empty V10() V11() V12() V13() V14() V15() V16() V17() V18() ) Element of NAT : ( ( ) ( V13() V14() V15() V16() V17() V18() V19() ) Element of K6(REAL : ( ( ) ( non empty V13() V14() V15() V19() V37() ) set ) ) : ( ( ) ( ) set ) ) ) = 1. TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( ) Element of the carrier of TernaryFieldEx : ( ( strict ) ( non empty strict ) TernaryFieldStr ) : ( ( ) ( non empty ) set ) ) ;

definition
let IT be ( ( non empty ) ( non empty ) TernaryFieldStr ) ;
attr IT is Ternary-Field-like means :: ALGSTR_3:def 5
( 0. IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) <> 1. IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) & ( for a being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) holds Tern (a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,(1. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ,(0. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for a being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) holds Tern ((1. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,(0. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for a, b being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) holds Tern (a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,(0. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for a, b being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) holds Tern ((0. IT : ( ( V42() ) ( V42() ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( V42() ) ( V42() ) set ) : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for u, a, b being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) ex v being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for u, a, v, v9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) holds
v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) = v9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) & ( for a, a9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) <> a9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) holds
for b, b9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) ex u, v being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st
( Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = b : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) & Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = b9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) ) & ( for u, u9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) <> u9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) holds
for v, v9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) ex a being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = Tern (u9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) ) & ( for a, a9, u, u9, v, v9 being ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) st Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = Tern (u9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) & Tern (u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) = Tern (u9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,a9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ,v9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) : ( ( ) ( ) Scalar of IT : ( ( V42() ) ( V42() ) set ) ) & not a : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) = a9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) holds
u : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) = u9 : ( ( ) ( ) Scalar of IT : ( ( non empty ) ( non empty ) TernaryFieldStr ) ) ) );
end;

registration
cluster non empty strict Ternary-Field-like for ( ( ) ( ) TernaryFieldStr ) ;
end;

definition
mode Ternary-Field is ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) TernaryFieldStr ) ;
end;

theorem :: ALGSTR_3:4
for F being ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field)
for a, a9, u, v, u9, v9 being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) <> a9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) & Tern (u : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,v : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = Tern (u9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,v9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) & Tern (u : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,v : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = Tern (u9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,v9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) holds
( u : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = u9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) & v : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = v9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) ;

theorem :: ALGSTR_3:5
for F being ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field)
for a being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) <> 0. F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( V56(b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) Element of the carrier of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( non empty ) set ) ) holds
for b, c being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ex x being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st Tern (a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = c : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ;

theorem :: ALGSTR_3:6
for F being ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field)
for a, x, b, x9 being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) <> 0. F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( V56(b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) Element of the carrier of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( non empty ) set ) ) & Tern (a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = Tern (a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,x9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) holds
x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = x9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ;

theorem :: ALGSTR_3:7
for F being ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field)
for a being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) <> 0. F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( V56(b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) Element of the carrier of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( non empty ) set ) ) holds
for b, c being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ex x being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st Tern (x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = c : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ;

theorem :: ALGSTR_3:8
for F being ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field)
for a, x, b, x9 being ( ( ) ( ) Scalar of F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) st a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) <> 0. F : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( V56(b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) Element of the carrier of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) : ( ( ) ( non empty ) set ) ) & Tern (x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = Tern (x9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,a : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ,b : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ) : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) holds
x : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) = x9 : ( ( ) ( ) Scalar of b1 : ( ( non empty Ternary-Field-like ) ( non empty Ternary-Field-like ) Ternary-Field) ) ;