:: deftheorem Def3 defines " MATRIX_7:def 4 :
for G being Group
for f, b₃ being FinSequence of G holds
( b₃ = f " iff ( len b₃ = len f & ( for i being Nat st i in dom f holds
b₃ /. i = (f /. i) " ) ) );