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);
reconsider f = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A1: ( Den o,(MSAlg U1) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, 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, 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