let U1 be Universal_Algebra; :: thesis: for o being OperSymbol of (MSSign U1)
for y being Element of Args o,(MSAlg U1) holds y is FinSequence of the carrier of U1
let o be OperSymbol of (MSSign U1); :: thesis: for y being Element of Args o,(MSAlg U1) holds y is FinSequence of the carrier of U1
let y be Element of Args o,(MSAlg U1); :: thesis: y is FinSequence of the carrier of U1
set O1 = Den o,(MSAlg U1);
A1: Den o,(MSAlg U1) = the charact of U1 . o by Th12;
reconsider f = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A2: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = f & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
dom (signature U1) = dom the charact of U1 by Lm1;
then reconsider O1 = Den o,(MSAlg U1) as operation of U1 by A1, A2, FUNCT_1:def 5;
Args o,(MSAlg U1) = dom O1 by FUNCT_2:def 1;
then y in the carrier of U1 * by TARSKI:def 3;
hence y is FinSequence of the carrier of U1 by FINSEQ_1:def 11; :: thesis: verum