set A = the non-empty MSAlgebra over S;
set f = I --> the non-empty MSAlgebra over S;
reconsider f = I --> the non-empty MSAlgebra over S as ManySortedSet of I ;
take f ; :: thesis: for i being object st i in I holds
f . i is non-empty MSAlgebra over S
let i be object ; :: thesis: ( i in I implies f . i is non-empty MSAlgebra over S )
assume i in I ; :: thesis: f . i is non-empty MSAlgebra over S
hence f . i is non-empty MSAlgebra over S by FUNCOP_1:7; :: thesis: verum