for i being Element of I holds (F ./. N) . i is strict Group

proof

let i be Element of I; :: thesis: (F ./. N) . i is strict Group
(F ./. N) . i = (F . i) ./. (N . i) by Def8;
hence (F ./. N) . i is strict Group ; :: thesis: verum

end;

hence F ./. N is componentwise_strict ; :: thesis: verum