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
proof
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;
dom ( the normF of X | X1) = X1 by A1, A2, RELAT_1:62;
hence the normF of X | X1 is Function of X1,REAL by A3, FUNCT_2:3; :: thesis: verum