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

not (TrivialOps f) . n is empty

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

h is homogeneous

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

A4:
for n being object st n in dom (TrivialOps f) holds
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;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

not (TrivialOps f) . n is empty

proof

for n being Nat
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;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

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

h is homogeneous

proof

hence
( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )
by A1, A4, FUNCT_1:def 9; :: thesis: verum
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;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