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 & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def 8;
dom (signature U1) = dom the charact of U1 by Lm1;
then reconsider O1 = Den (o,(MSAlg U1)) as operation of U1 by A1, FUNCT_1:def 3;
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