let V be free Z_Module; :: thesis: for A, B being Subset of V st A c= B & B is Basis of V holds
ex F being linear-transformation of V,V st
( ( 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 & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) )
let A, B be Subset of V; :: thesis: ( A c= B & B is Basis of V implies ex F being linear-transformation of V,V st
( ( 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 & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) ) )
assume ( A c= B & B is Basis of V ) ; :: thesis: ex F being linear-transformation of V,V st
( ( 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 & F . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F . v = vA ) )
then P0: V is_the_direct_sum_of Lin A, Lin (B \ A) by ZMODUL05:50;
defpred S₁[ Element of V, object ] means ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & $1 = vA + vB & $2 = vA );
A1: for v being Element of V ex vA being Element of V st S₁[v,vA]

proof

let v be Element of V; :: thesis: ex vA being Element of V st S₁[v,vA]
consider vA, vB being Vector of V such that
A2: ( vA in Lin A & vB in Lin (B \ A) & v = vA + vB ) by P0, ZMODUL01:133;
take vA ; :: thesis: S₁[v,vA]
thus S₁[v,vA] by A2; :: thesis: verum

end;

consider f being Function of V,V such that
A9: for v being Vector of V holds S₁[v,f . v] from FUNCT_2:sch 3(A1);
A10: for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA

proof

let v, vA, vB be Vector of V; :: thesis: ( vA in Lin A & vB in Lin (B \ A) & v = vA + vB implies f . v = vA )
assume A11: ( vA in Lin A & vB in Lin (B \ A) & v = vA + vB ) ; :: thesis: f . v = vA
consider vA1, vB1 being Vector of V such that
A12: ( vA1 in Lin A & vB1 in Lin (B \ A) & v = vA1 + vB1 & f . v = vA1 ) by A9;
thus f . v = vA by A11, A12, P0, ZMODUL01:134; :: thesis: verum

end;

A13: f is additive

proof

let x, y be Element of V; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)
consider xA, xB being Vector of V such that
A14: ( xA in Lin A & xB in Lin (B \ A) & x = xA + xB & f . x = xA ) by A9;
consider yA, yB being Vector of V such that
A15: ( yA in Lin A & yB in Lin (B \ A) & y = yA + yB & f . y = yA ) by A9;
consider xyA, xyB being Vector of V such that
A16: ( xyA in Lin A & xyB in Lin (B \ A) & x + y = xyA + xyB & f . (x + y) = xyA ) by A9;
A17: xyA + xyB = ((xA + xB) + yA) + yB by A14, A15, A16, RLVECT_1:def 3
.= (xB + (xA + yA)) + yB by RLVECT_1:def 3
.= (xA + yA) + (xB + yB) by RLVECT_1:def 3 ;
A18: xA + yA in Lin A by A14, A15, ZMODUL01:36;
xB + yB in Lin (B \ A) by A14, A15, ZMODUL01:36;
hence f . (x + y) = (f . x) + (f . y) by A14, A15, A16, A17, A18, P0, ZMODUL01:134; :: thesis: verum

end;

for r being Element of INT.Ring
for x being Element of V holds f . (r * x) = r * (f . x)

proof

let r be Element of INT.Ring; :: thesis: for x being Element of V holds f . (r * x) = r * (f . x)
let x be Element of V; :: thesis: f . (r * x) = r * (f . x)
consider xA, xB being Vector of V such that
A14: ( xA in Lin A & xB in Lin (B \ A) & x = xA + xB & f . x = xA ) by A9;
consider rxA, rxB being Vector of V such that
A15: ( rxA in Lin A & rxB in Lin (B \ A) & r * x = rxA + rxB & f . (r * x) = rxA ) by A9;
A16: rxA + rxB = (r * xA) + (r * xB) by A14, A15, VECTSP_1:def 14;
A18: r * xA in Lin A by A14, ZMODUL01:37;
r * xB in Lin (B \ A) by A14, ZMODUL01:37;
hence f . (r * x) = r * (f . x) by A14, A15, A16, A18, P0, ZMODUL01:134; :: thesis: verum

end;

then f is homogeneous ;
then reconsider f = f as linear-transformation of V,V by A13;
take f ; :: thesis: ( ( 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 & f . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA ) )
thus ( ( 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 & f . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
f . v = vA ) ) by A10, A9; :: thesis: verum