deffunc H₁( Element of [:F₁(),F₂():], Element of [:F₁(),F₂():]) -> Element of F₃() = F₄(($1 `1),($2 `1),($1 `2),($2 `2));
consider f being Function of [:[:F₁(),F₂():],[:F₁(),F₂():]:],F₃() such that
A1: for x, y being Element of [:F₁(),F₂():] holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x1, y1 being Element of F₁()
for x2, y2 being Element of F₂()
for x, y being Element of [:F₁(),F₂():] st x = [x1,x2] & y = [y1,y2] holds
f . (x,y) = F₄(x1,y1,x2,y2)
let x1, y1 be Element of F₁(); :: thesis: for x2, y2 being Element of F₂()
for x, y being Element of [:F₁(),F₂():] st x = [x1,x2] & y = [y1,y2] holds
f . (x,y) = F₄(x1,y1,x2,y2)
let x2, y2 be Element of F₂(); :: thesis: for x, y being Element of [:F₁(),F₂():] st x = [x1,x2] & y = [y1,y2] holds
f . (x,y) = F₄(x1,y1,x2,y2)
let x, y be Element of [:F₁(),F₂():]; :: thesis: ( x = [x1,x2] & y = [y1,y2] implies f . (x,y) = F₄(x1,y1,x2,y2) )
assume that
A2: x = [x1,x2] and
A3: y = [y1,y2] ; :: thesis: f . (x,y) = F₄(x1,y1,x2,y2)
A4: ( y1 = y `1 & y2 = y `2 ) by A3;
( x1 = x `1 & x2 = x `2 ) by A2;
hence f . (x,y) = F₄(x1,y1,x2,y2) by A1, A4; :: thesis: verum