defpred S₁[ set , set , set ] means ex x9, y9 being Element of n -tuples_on D st
( $1 = x9 & $2 = y9 & $3 = F .: (x9,y9) );
A1: for x, y being Element of n -tuples_on D ex z being Element of n -tuples_on D st S₁[x,y,z]

proof

let x, y be Element of n -tuples_on D; :: thesis: ex z being Element of n -tuples_on D st S₁[x,y,z]
reconsider x9 = x, y9 = y as Element of n -tuples_on D ;
reconsider z = F .: (x9,y9) as Element of n -tuples_on D ;
take z ; :: thesis: S₁[x,y,z]
take x9 ; :: thesis: ex y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & z = F .: (x9,y9) )
take y9 ; :: thesis: ( x = x9 & y = y9 & z = F .: (x9,y9) )
thus ( x = x9 & y = y9 & z = F .: (x9,y9) ) ; :: thesis: verum

end;

consider G being BinOp of (n -tuples_on D) such that
A2: for x, y being Element of n -tuples_on D holds S₁[x,y,G . (x,y)] from BINOP_1:sch 3(A1);
take G ; :: thesis: for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y)
let p1, p2 be Element of n -tuples_on D; :: thesis: G . (p1,p2) = F .: (p1,p2)
reconsider x = p1, y = p2 as Element of n -tuples_on D ;
ex x9, y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & G . (x,y) = F .: (x9,y9) ) by A2;
hence G . (p1,p2) = F .: (p1,p2) ; :: thesis: verum