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 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 A2: ( n in dom (TrivialOps f) & (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 A2, FINSEQ_2:13;
(TrivialOps f) . n = TrivialOp m by A2, Def8;
hence h is homogeneous by A2; :: thesis: verum

end;

A3: 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 A4: ( n in dom (TrivialOps f) & (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 A4, FINSEQ_2:13;
(TrivialOps f) . n = TrivialOp m by A4, Def8;
hence h is quasi_total by A4; :: thesis: verum

end;

for n being set st n in dom (TrivialOps f) holds
not (TrivialOps f) . n is empty

proof

let n be set ; :: 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:13;
(TrivialOps f) . k = TrivialOp m by A5, Def8;
hence not (TrivialOps f) . n is empty ; :: thesis: verum

end;

hence ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) by A1, A3, FUNCT_1:def 15, UNIALG_1:def 4, UNIALG_1:def 5; :: thesis: verum