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

proof

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

end;

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