reconsider G = multMagma(# REAL,addreal #) as strict Group by GROUP_1:46;
deffunc H₁( Element of I) -> strict Group = G;
consider F being Group-Family of I such that
A1: for i being Element of I holds F . i = H₁(i) from GROUP_23:sch 1();
take F ; :: thesis: F is componentwise_strict
thus F is componentwise_strict by A1; :: thesis: verum