defpred S_{1}[ set , set ] means for m being Nat st m = f . $1 holds

$2 = TrivialOp m;

A1: for k being Nat st k in Seg (len f) holds

ex x being Element of PFuncs (({{}} *),{{}}) st S_{1}[k,x]

A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds

S_{1}[k,p . k] ) )
from FINSEQ_1:sch 5(A1);

reconsider p = p as PFuncFinSequence of {{}} ;

take p ; :: thesis: ( len p = len f & ( for n being Nat st n in dom p holds

for m being Nat st m = f . n holds

p . n = TrivialOp m ) )

thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom p holds

for m being Nat st m = f . n holds

p . n = TrivialOp m

let n be Nat; :: thesis: ( n in dom p implies for m being Nat st m = f . n holds

p . n = TrivialOp m )

assume n in dom p ; :: thesis: for m being Nat st m = f . n holds

p . n = TrivialOp m

hence for m being Nat st m = f . n holds

p . n = TrivialOp m by A2; :: thesis: verum

$2 = TrivialOp m;

A1: for k being Nat st k in Seg (len f) holds

ex x being Element of PFuncs (({{}} *),{{}}) st S

proof

consider p being FinSequence of PFuncs (({{}} *),{{}}) such that
let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of PFuncs (({{}} *),{{}}) st S_{1}[k,x] )

assume k in Seg (len f) ; :: thesis: ex x being Element of PFuncs (({{}} *),{{}}) st S_{1}[k,x]

then k in dom f by FINSEQ_1:def 3;

then reconsider k1 = f . k as Element of NAT by FINSEQ_2:11;

reconsider A = TrivialOp k1 as Element of PFuncs (({{}} *),{{}}) by PARTFUN1:45;

take A ; :: thesis: S_{1}[k,A]

let m be Nat; :: thesis: ( m = f . k implies A = TrivialOp m )

assume m = f . k ; :: thesis: A = TrivialOp m

hence A = TrivialOp m ; :: thesis: verum

end;assume k in Seg (len f) ; :: thesis: ex x being Element of PFuncs (({{}} *),{{}}) st S

then k in dom f by FINSEQ_1:def 3;

then reconsider k1 = f . k as Element of NAT by FINSEQ_2:11;

reconsider A = TrivialOp k1 as Element of PFuncs (({{}} *),{{}}) by PARTFUN1:45;

take A ; :: thesis: S

let m be Nat; :: thesis: ( m = f . k implies A = TrivialOp m )

assume m = f . k ; :: thesis: A = TrivialOp m

hence A = TrivialOp m ; :: thesis: verum

A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds

S

reconsider p = p as PFuncFinSequence of {{}} ;

take p ; :: thesis: ( len p = len f & ( for n being Nat st n in dom p holds

for m being Nat st m = f . n holds

p . n = TrivialOp m ) )

thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom p holds

for m being Nat st m = f . n holds

p . n = TrivialOp m

let n be Nat; :: thesis: ( n in dom p implies for m being Nat st m = f . n holds

p . n = TrivialOp m )

assume n in dom p ; :: thesis: for m being Nat st m = f . n holds

p . n = TrivialOp m

hence for m being Nat st m = f . n holds

p . n = TrivialOp m by A2; :: thesis: verum