scheme :: AIMLOOP:sch 1
MltInd{ F1() -> multLoop, F2() -> Subset of F1(), P1[ Function of F1(),F1()] } :
for f being Function of F1(),F1() st f in Mlt F2() holds
P1[f]
provided
A1: for u being Element of F1() st u in F2() holds
for f being Function of F1(),F1() st ( for x being Element of F1() holds f . x = x * u ) holds
P1[f] and
A2: for u being Element of F1() st u in F2() holds
for f being Function of F1(),F1() st ( for x being Element of F1() holds f . x = u * x ) holds
P1[f] and
A3: for g, h being Permutation of F1() st P1[g] & P1[h] holds
P1[g * h] and
A4: for g being Permutation of F1() st P1[g] holds
P1[g " ]