let f be FinSequence of NAT ; :: thesis: ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )
A1: for n being Nat
for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is quasi_total

proof

let n be Nat; :: thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is quasi_total
let h be PartFunc of ({{}} *),{{}}; :: thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is quasi_total )
assume that
A2: n in dom (TrivialOps f) and
A3: (TrivialOps f) . n = h ; :: thesis: h is quasi_total
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def 3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def 3 ;
then reconsider m = f . n as Element of NAT by A2, FINSEQ_2:11;
(TrivialOps f) . n = TrivialOp m by A2, Def8;
hence h is quasi_total by A3; :: thesis: verum

end;

A4: for n being object st n in dom (TrivialOps f) holds
not (TrivialOps f) . n is empty

proof

let n be object ; :: thesis: ( n in dom (TrivialOps f) implies not (TrivialOps f) . n is empty )
assume A5: n in dom (TrivialOps f) ; :: thesis: not (TrivialOps f) . n is empty
then reconsider k = n as Element of NAT ;
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def 3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def 3 ;
then reconsider m = f . k as Element of NAT by A5, FINSEQ_2:11;
(TrivialOps f) . k = TrivialOp m by A5, Def8;
hence not (TrivialOps f) . n is empty ; :: thesis: verum

end;

for n being Nat
for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is homogeneous

proof

let n be Nat; :: thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds
h is homogeneous
let h be PartFunc of ({{}} *),{{}}; :: thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is homogeneous )
assume that
A6: n in dom (TrivialOps f) and
A7: (TrivialOps f) . n = h ; :: thesis: h is homogeneous
dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def 3
.= Seg (len f) by Def8
.= dom f by FINSEQ_1:def 3 ;
then reconsider m = f . n as Element of NAT by A6, FINSEQ_2:11;
(TrivialOps f) . n = TrivialOp m by A6, Def8;
hence h is homogeneous by A7; :: thesis: verum

end;

hence ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) by A1, A4, FUNCT_1:def 9; :: thesis: verum