deffunc H₁( Element of the_set_of_ComplexSequences , Element of the_set_of_ComplexSequences ) -> Element of bool [:NAT ,COMPLEX :] = (seq_id $1) + (seq_id $2);
for o1, o2 being BinOp of the_set_of_ComplexSequences st ( for a, b being Element of the_set_of_ComplexSequences holds o1 . a,b = H₁(a,b) ) & ( for a, b being Element of the_set_of_ComplexSequences holds o2 . a,b = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2();
hence for b₁, b₂ being BinOp of the_set_of_ComplexSequences st ( for a, b being Element of the_set_of_ComplexSequences holds b₁ . a,b = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_ComplexSequences holds b₂ . a,b = (seq_id a) + (seq_id b) ) holds
b₁ = b₂ ; :: thesis: verum