A2:
dom the normF of X = the carrier of X
by FUNCT_2:def 1;

A3: for z being object st z in X1 holds

( the normF of X | X1) . z in REAL

hence the normF of X | X1 is Function of X1,REAL by A3, FUNCT_2:3; :: thesis: verum

A3: for z being object st z in X1 holds

( the normF of X | X1) . z in REAL

proof

dom ( the normF of X | X1) = X1
by A1, A2, RELAT_1:62;
let z be object ; :: thesis: ( z in X1 implies ( the normF of X | X1) . z in REAL )

assume A4: z in X1 ; :: thesis: ( the normF of X | X1) . z in REAL

then reconsider y = z as VECTOR of X by A1;

z in dom ( the normF of X | X1) by A1, A2, A4, RELAT_1:62;

then ( the normF of X | X1) . z = ||.y.|| by FUNCT_1:47;

hence ( the normF of X | X1) . z in REAL ; :: thesis: verum

end;assume A4: z in X1 ; :: thesis: ( the normF of X | X1) . z in REAL

then reconsider y = z as VECTOR of X by A1;

z in dom ( the normF of X | X1) by A1, A2, A4, RELAT_1:62;

then ( the normF of X | X1) . z = ||.y.|| by FUNCT_1:47;

hence ( the normF of X | X1) . z in REAL ; :: thesis: verum

hence the normF of X | X1 is Function of X1,REAL by A3, FUNCT_2:3; :: thesis: verum