set f = TrivialOp k;
A1: dom (TrivialOp k) = {(k |-> {})} by Def7;
thus TrivialOp k is homogeneous :: thesis: ( TrivialOp k is quasi_total & not TrivialOp k is empty )

proof

let x, y be FinSequence; :: according to MARGREL1:def 1,MARGREL1:def 21 :: thesis: ( not x in proj1 (TrivialOp k) or not y in proj1 (TrivialOp k) or len x = len y )
assume that
A2: x in dom (TrivialOp k) and
A3: y in dom (TrivialOp k) ; :: thesis: len x = len y
x = k |-> {} by A1, A2, TARSKI:def 1;
hence len x = len y by A1, A3, TARSKI:def 1; :: thesis: verum

end;

now

let x, y be FinSequence of {{}}; :: thesis: ( len x = len y & x in dom (TrivialOp k) implies y in dom (TrivialOp k) )
assume that
A4: len x = len y and
A5: x in dom (TrivialOp k) ; :: thesis: y in dom (TrivialOp k)
A6: dom x = Seg (len x) by FINSEQ_1:def 3;
A7: x = k |-> {} by A1, A5, TARSKI:def 1;
then A8: len x = k by CARD_1:def 7;

now

let n be Nat; :: thesis: ( n in dom x implies x . n = y . n )
assume A9: n in dom x ; :: thesis: x . n = y . n
then n in dom y by A4, A6, FINSEQ_1:def 3;
then A10: y . n in {{}} by FINSEQ_2:11;
x . n = {} by A7, A8, A6, A9, FUNCOP_1:7;
hence x . n = y . n by A10, TARSKI:def 1; :: thesis: verum

end;

hence y in dom (TrivialOp k) by A4, A5, FINSEQ_2:9; :: thesis: verum

end;

hence ( TrivialOp k is quasi_total & not TrivialOp k is empty ) by A1, MARGREL1:def 22; :: thesis: verum