deffunc H_{1}( Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():], Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():]) -> Element of F_{5}() = F_{6}(($1 `1_4),($2 `1_4),($1 `2_4),($2 `2_4),($1 `3_4),($2 `3_4),($1 `4_4),($2 `4_4));

consider f being Function of [:[:F_{1}(),F_{2}(),F_{3}(),F_{4}():],[:F_{1}(),F_{2}(),F_{3}(),F_{4}():]:],F_{5}() such that

A1: for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

take f ; :: thesis: for x1, y1 being Element of F_{1}()

for x2, y2 being Element of F_{2}()

for x3, y3 being Element of F_{3}()

for x4, y4 being Element of F_{4}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

let x1, y1 be Element of F_{1}(); :: thesis: for x2, y2 being Element of F_{2}()

for x3, y3 being Element of F_{3}()

for x4, y4 being Element of F_{4}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

let x2, y2 be Element of F_{2}(); :: thesis: for x3, y3 being Element of F_{3}()

for x4, y4 being Element of F_{4}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

let x3, y3 be Element of F_{3}(); :: thesis: for x4, y4 being Element of F_{4}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

let x4, y4 be Element of F_{4}(); :: thesis: for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

let x, y be Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():]; :: thesis: ( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] implies f . (x,y) = F_{6}(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_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

A5: ( y1 = y `1_4 & y2 = y `2_4 ) by A3;

A7: ( x3 = x `3_4 & x4 = x `4_4 ) by A2;

A8: ( y3 = y `3_4 & y4 = y `4_4 ) by A3;

( x1 = x `1_4 & x2 = x `2_4 ) by A2;

hence f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)
by A1, A5, A7, A8; :: thesis: verum

consider f being Function of [:[:F

A1: for x, y being Element of [:F

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 . (x,y) = F

let x1, y1 be 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 . (x,y) = F

let x2, y2 be Element of F

for x4, y4 being Element of F

for x, y being Element of [:F

f . (x,y) = F

let x3, y3 be Element of F

for x, y being Element of [:F

f . (x,y) = F

let x4, y4 be Element of F

f . (x,y) = F

let x, y be Element of [:F

assume that

A2: x = [x1,x2,x3,x4] and

A3: y = [y1,y2,y3,y4] ; :: thesis: f . (x,y) = F

A5: ( y1 = y `1_4 & y2 = y `2_4 ) by A3;

A7: ( x3 = x `3_4 & x4 = x `4_4 ) by A2;

A8: ( y3 = y `3_4 & y4 = y `4_4 ) by A3;

( x1 = x `1_4 & x2 = x `2_4 ) by A2;

hence f . (x,y) = F