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

now :: thesis: for x, y being FinSequence of {{}} st len x = len y & x in dom (TrivialOp k) holds
y in dom (TrivialOp k)

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

now :: thesis: for n being Nat st n in dom x holds
x . n = y . n

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

end;

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

end;

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