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 )

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)

hence
( TrivialOp k is quasi_total & not TrivialOp k is empty )
by A1; :: thesis: verumy 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;

end;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

hence
y in dom (TrivialOp k)
by A2, A3, FINSEQ_2:9; :: thesis: verumx . 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;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