set Y = VAR \/ GRZ-ops;
for a being object st a in VAR \/ GRZ-ops holds
a is FinSequence
proof
let a be object ; :: thesis: ( a in VAR \/ GRZ-ops implies a is FinSequence )
assume A1: a in VAR \/ GRZ-ops ; :: thesis: a is FinSequence
A2: ( a in VAR implies a is FinSequence ) ;
( a in GRZ-ops implies a is FinSequence ) ;
hence a is FinSequence by A1, A2, XBOOLE_0:def 3; :: thesis: verum
end;
hence VAR \/ GRZ-ops is non empty FinSequence-membered set by FINSEQ_1:def 18; :: thesis: verum