:: deftheorem Def1 defines => HILBERT3:def 1 :
for A, B being non empty set
for P being Permutation of A
for Q being Function of B,B
for b₅ being Function of (Funcs (A,B)),(Funcs (A,B)) holds
( b₅ = P => Q iff for f being Function of A,B holds b₅ . f = (Q * f) * (P ") );