deffunc H₁( Element of [:F₁(),F₂(),F₃(),F₄():], Element of [:F₁(),F₂(),F₃(),F₄():]) -> Element of F₅() = F₆(($1 `1),($2 `1),($1 `2),($2 `2),($1 `3),($2 `3),($1 `4),($2 `4));
consider f being Function of [:[:F₁(),F₂(),F₃(),F₄():],[:F₁(),F₂(),F₃(),F₄():]:],F₅() such that
A1: for x, y being Element of [:F₁(),F₂(),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 x3, y3 being Element of F₃()
for x4, y4 being Element of F₄()
for x, y being Element of [:F₁(),F₂(),F₃(),F₄():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
let x1, y1 be Element of F₁(); :: thesis: for x2, y2 being Element of F₂()
for x3, y3 being Element of F₃()
for x4, y4 being Element of F₄()
for x, y being Element of [:F₁(),F₂(),F₃(),F₄():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
let x2, y2 be Element of F₂(); :: thesis: for x3, y3 being Element of F₃()
for x4, y4 being Element of F₄()
for x, y being Element of [:F₁(),F₂(),F₃(),F₄():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
let x3, y3 be Element of F₃(); :: thesis: for x4, y4 being Element of F₄()
for x, y being Element of [:F₁(),F₂(),F₃(),F₄():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
let x4, y4 be Element of F₄(); :: thesis: for x, y being Element of [:F₁(),F₂(),F₃(),F₄():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
let x, y be Element of [:F₁(),F₂(),F₃(),F₄():]; :: thesis: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] implies f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4) )
assume that
A2: x = [x1,x2,x3,x4] and
A3: y = [y1,y2,y3,y4] ; :: thesis: f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4)
A4: y = [(y `1),(y `2),(y `3),(y `4)] by MCART_1:56;
then A5: ( y1 = y `1 & y2 = y `2 ) by A3, MCART_1:29;
A6: x = [(x `1),(x `2),(x `3),(x `4)] by MCART_1:56;
then A7: ( x3 = x `3 & x4 = x `4 ) by A2, MCART_1:29;
A8: ( y3 = y `3 & y4 = y `4 ) by A3, A4, MCART_1:29;
( x1 = x `1 & x2 = x `2 ) by A2, A6, MCART_1:29;
hence f . (x,y) = F₆(x1,y1,x2,y2,x3,y3,x4,y4) by A1, A5, A7, A8; :: thesis: verum