deffunc H₂( Element of H₁(F), Element of H₁(F)) -> Element of [:the carrier of F,the carrier of F,the carrier of F:] = [(($1 `1 ) + ($2 `1 )),(($1 `2 ) + ($2 `2 )),(($1 `3 ) + ($2 `3 ))];
consider f being BinOp of H₁(F) such that
A1: for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x,y = H₂(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))]
thus for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))] by A1; :: thesis: verum