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