consider A being non-empty MSAlgebra of S;
set f = I --> A;
( dom (I --> A) = I & ( for i being set st i in I holds
(I --> A) . i = A ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider f = I --> A as ManySortedSet of by PARTFUN1:def 4;
take f ; :: thesis: for i being set st i in I holds
f . i is non-empty MSAlgebra of S
let i be set ; :: thesis: ( i in I implies f . i is non-empty MSAlgebra of S )
assume i in I ; :: thesis: f . i is non-empty MSAlgebra of S
hence f . i is non-empty MSAlgebra of S by FUNCOP_1:13; :: thesis: verum