:: deftheorem defines Proj ZMATRLIN:def 10 :
for V being free Z_Module
for A, B being Subset of V st A c= B & B is Basis of V holds
for b₄ being linear-transformation of V,V holds
( b₄ = Proj (A,B) iff ( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b₄ . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
b₄ . v = vA ) ) );