defpred S₁[ object , object ] means ex q being FinSequence st
( $1 = q & $2 = p ^ q );
A10: for a being object st a in Z holds
ex b being object st
( b in Z & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in Z implies ex b being object st
( b in Z & S₁[a,b] ) )
assume A11: a in Z ; :: thesis: ex b being object st
( b in Z & S₁[a,b] )
then reconsider q = a as FinSequence ;
A12: q in Z ^^ 1 by A11;
take b = p ^ q; :: thesis: ( b in Z & S₁[a,b] )
Z is B -closed ;
hence b in Z by A1, A12; :: thesis: S₁[a,b]
thus S₁[a,b] ; :: thesis: verum

end;

consider f being Function of Z,Z such that
A20: for a being object st a in Z holds
S₁[a,f . a] from FUNCT_2:sch 1(A10);
reconsider f = f as UnOp of Z ;
take f ; :: thesis: for q being FinSequence st q in Z holds
f . q = p ^ q
let q be FinSequence; :: thesis: ( q in Z implies f . q = p ^ q )
assume q in Z ; :: thesis: f . q = p ^ q
then consider s being FinSequence such that
A22: ( q = s & f . q = p ^ s ) by A20;
thus f . q = p ^ q by A22; :: thesis: verum