let F1, F2 be linear-transformation of V,V; :: 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 & F1 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F1 . v = vA ) & ( 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 & F2 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F2 . v = vA ) implies F1 = F2 )
assume A1: ( ( 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 & F1 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F1 . v = vA ) ) ; :: thesis: ( ex v being Vector of V st
for vA, vB being Vector of V holds
( not vA in Lin A or not vB in Lin (B \ A) or not v = vA + vB or not F2 . v = vA ) or ex v, vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & not F2 . v = vA ) or F1 = F2 )
assume A2: ( ( 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 & F2 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
F2 . v = vA ) ) ; :: thesis: F1 = F2
now :: thesis: for v being Vector of V holds F1 . v = F2 . v
let v be Vector of V; :: thesis: F1 . v = F2 . v
consider vA, vB being Vector of V such that
A3: ( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & F1 . v = vA ) by A1;
thus F1 . v = F2 . v by A2, A3; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:def 7; :: thesis: verum