let S0 be non empty non void strict all-with_const_op ManySortedSign ; :: thesis: OSSign S0 is all-with_const_op
let s be Element of (OSSign S0); :: according to MSUALG_2:def 2 :: thesis: s is with_const_op
reconsider s1 = s as Element of S0 by OSALG_1:def 5;
s1 is with_const_op by MSUALG_2:def 2;
then consider o being Element of the carrier' of S0 such that
A1: ( the Arity of S0 . o = {} & the ResultSort of S0 . o = s1 ) ;
A2: o is Element of the carrier' of (OSSign S0) by OSALG_1:def 5;
( the Arity of (OSSign S0) . o = {} & the ResultSort of (OSSign S0) . o = s1 ) by A1, OSALG_1:def 5;
hence s is with_const_op by A2; :: thesis: verum