:: deftheorem Def4 defines Opers PRALG_1:def 4 :
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for b₃ being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds
( b₃ = Opers (U1,U2) iff ( len b₃ = len the charact of U1 & ( for n being Nat st n in dom b₃ holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b₃ . n = [[:h1,h2:]] ) ) );