let f be FinSequence of NAT ; :: thesis:
A1: for n being Nat
for h being PartFunc of (), st n in dom () & h = () . n holds
h is quasi_total
proof
let n be Nat; :: thesis: for h being PartFunc of (), st n in dom () & h = () . n holds
h is quasi_total

let h be PartFunc of (),; :: thesis: ( n in dom () & h = () . n implies h is quasi_total )
assume that
A2: n in dom () and
A3: (TrivialOps f) . n = h ; :: thesis: h is quasi_total
dom () = Seg (len ()) 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 ;
(TrivialOps f) . n = TrivialOp m by ;
hence h is quasi_total by A3; :: thesis: verum
end;
A4: for n being object st n in dom () holds
not () . n is empty
proof
let n be object ; :: thesis: ( n in dom () implies not () . n is empty )
assume A5: n in dom () ; :: thesis: not () . n is empty
then reconsider k = n as Element of NAT ;
dom () = Seg (len ()) 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 ;
(TrivialOps f) . k = TrivialOp m by ;
hence not (TrivialOps f) . n is empty ; :: thesis: verum
end;
for n being Nat
for h being PartFunc of (), st n in dom () & h = () . n holds
h is homogeneous
proof
let n be Nat; :: thesis: for h being PartFunc of (), st n in dom () & h = () . n holds
h is homogeneous

let h be PartFunc of (),; :: thesis: ( n in dom () & h = () . n implies h is homogeneous )
assume that
A6: n in dom () and
A7: (TrivialOps f) . n = h ; :: thesis: h is homogeneous
dom () = Seg (len ()) 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 ;
(TrivialOps f) . n = TrivialOp m by ;
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 ; :: thesis: verum