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