let n be Nat; :: thesis: for D being non empty set

for H, G being BinOp of D

for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let D be non empty set ; :: thesis: for H, G being BinOp of D

for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let H, G be BinOp of D; :: thesis: for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let d be Element of D; :: thesis: for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let t1, t2 be Element of n -tuples_on D; :: thesis: ( H is_distributive_wrt G implies H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) )

( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H ) by RELAT_1:26;

then ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] & [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] c= [:(rng H),(rng H):] ) by FUNCT_3:51, ZFMISC_1:96;

then A1: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):] by XBOOLE_1:1;

rng H c= D by RELAT_1:def 19;

then [:(rng H),(rng H):] c= [:D,D:] by ZFMISC_1:96;

then rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:] by A1, XBOOLE_1:1;

then A2: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G by FUNCT_2:def 1;

A3: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;

then A4: [:(rng t1),(rng t2):] c= [:D,D:] by ZFMISC_1:96;

rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:51;

then rng <:t1,t2:> c= [:D,D:] by A4, XBOOLE_1:1;

then A5: rng <:t1,t2:> c= dom G by FUNCT_2:def 1;

A6: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13

.= Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then dom <:t1,t2:> = Seg n by A3, FUNCT_3:50;

then A7: dom (G * <:t1,t2:>) = Seg n by A5, RELAT_1:27;

then dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:13;

then A8: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A7, FUNCT_3:50;

rng t2 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A9: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;

rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A10: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A9, XBOOLE_1:1;

A11: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

rng t1 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A12: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;

rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A13: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A12, XBOOLE_1:1;

A14: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13

.= Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

{d} c= D by ZFMISC_1:31;

then A15: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:13, ZFMISC_1:31;

then A16: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;

A17: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom H = [:D,D:] by FUNCT_2:def 1;

then A18: dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A10, A15, RELAT_1:27, XBOOLE_1:1

.= Seg n by A6, A17, FUNCT_3:50 ;

{d} c= D by ZFMISC_1:31;

then A19: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A13, A19, RELAT_1:27, XBOOLE_1:1

.= Seg n by A14, A11, FUNCT_3:50 ;

then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A18, FUNCT_3:50;

then A20: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A2, RELAT_1:27;

rng (G * <:t1,t2:>) c= D by RELAT_1:def 19;

then ( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] & [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] ) by A16, FUNCT_3:51, ZFMISC_1:96;

then rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] by XBOOLE_1:1;

then A21: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H by FUNCT_2:def 1;

then A22: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A8, RELAT_1:27;

assume A23: H is_distributive_wrt G ; :: thesis: H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

for x being object st x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) holds

(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x

for H, G being BinOp of D

for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let D be non empty set ; :: thesis: for H, G being BinOp of D

for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let H, G be BinOp of D; :: thesis: for d being Element of D

for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let d be Element of D; :: thesis: for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds

H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

let t1, t2 be Element of n -tuples_on D; :: thesis: ( H is_distributive_wrt G implies H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) )

( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H ) by RELAT_1:26;

then ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] & [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] c= [:(rng H),(rng H):] ) by FUNCT_3:51, ZFMISC_1:96;

then A1: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):] by XBOOLE_1:1;

rng H c= D by RELAT_1:def 19;

then [:(rng H),(rng H):] c= [:D,D:] by ZFMISC_1:96;

then rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:] by A1, XBOOLE_1:1;

then A2: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G by FUNCT_2:def 1;

A3: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;

then A4: [:(rng t1),(rng t2):] c= [:D,D:] by ZFMISC_1:96;

rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:51;

then rng <:t1,t2:> c= [:D,D:] by A4, XBOOLE_1:1;

then A5: rng <:t1,t2:> c= dom G by FUNCT_2:def 1;

A6: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13

.= Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then dom <:t1,t2:> = Seg n by A3, FUNCT_3:50;

then A7: dom (G * <:t1,t2:>) = Seg n by A5, RELAT_1:27;

then dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:13;

then A8: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A7, FUNCT_3:50;

rng t2 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A9: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;

rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A10: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A9, XBOOLE_1:1;

A11: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

rng t1 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A12: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;

rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A13: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A12, XBOOLE_1:1;

A14: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13

.= Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

{d} c= D by ZFMISC_1:31;

then A15: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:13, ZFMISC_1:31;

then A16: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;

A17: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom H = [:D,D:] by FUNCT_2:def 1;

then A18: dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A10, A15, RELAT_1:27, XBOOLE_1:1

.= Seg n by A6, A17, FUNCT_3:50 ;

{d} c= D by ZFMISC_1:31;

then A19: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A13, A19, RELAT_1:27, XBOOLE_1:1

.= Seg n by A14, A11, FUNCT_3:50 ;

then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A18, FUNCT_3:50;

then A20: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A2, RELAT_1:27;

rng (G * <:t1,t2:>) c= D by RELAT_1:def 19;

then ( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] & [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] ) by A16, FUNCT_3:51, ZFMISC_1:96;

then rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] by XBOOLE_1:1;

then A21: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H by FUNCT_2:def 1;

then A22: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A8, RELAT_1:27;

assume A23: H is_distributive_wrt G ; :: thesis: H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))

for x being object st x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) holds

(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x

proof

hence
H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
by A8, A21, A20, RELAT_1:27; :: thesis: verum
rng t1 c= D
by FINSEQ_1:def 4;

then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A24: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;

rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A25: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A24, XBOOLE_1:1;

A26: ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;

{d} c= D by ZFMISC_1:31;

then A27: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

A28: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13

.= Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

{d} c= D by ZFMISC_1:31;

then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

A30: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

rng t2 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A31: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;

rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A32: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A31, XBOOLE_1:1;

A33: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13

.= Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

let x be object ; :: thesis: ( x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) implies (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x )

A34: dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> = (dom ((dom (G .: (t1,t2))) --> d)) /\ (dom (G .: (t1,t2))) by FUNCT_3:def 7;

assume A35: x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) ; :: thesis: (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x

then x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> by FUNCT_1:11;

then A36: x in dom (G .: (t1,t2)) by A34, XBOOLE_0:def 4;

dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then A37: t1 . x in rng t1 by A22, A35, FUNCT_1:def 3;

A38: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A25, A29, RELAT_1:27, XBOOLE_1:1

.= Seg n by A33, A30, FUNCT_3:50 ;

then A39: x in dom (H [;] (d,t1)) by A22, A35;

dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then A40: t2 . x in rng t2 by A22, A35, FUNCT_1:def 3;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A32, A27, RELAT_1:27, XBOOLE_1:1

.= Seg n by A28, A38, FUNCT_3:50 ;

then A41: x in dom (H [;] (d,t2)) by A22, A35;

(H [;] (d,(G .: (t1,t2)))) . x = H . (d,((G .: (t1,t2)) . x)) by A35, FUNCOP_1:32

.= H . (d,(G . ((t1 . x),(t2 . x)))) by A36, FUNCOP_1:22

.= G . ((H . (d,(t1 . x))),(H . (d,(t2 . x)))) by A23, A37, A26, A40, BINOP_1:11

.= G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x)))) by A39, FUNCOP_1:32

.= G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x)) by A41, FUNCOP_1:32

.= (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x by A22, A20, A35, FUNCOP_1:22 ;

hence (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x ; :: thesis: verum

end;then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A24: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;

rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A25: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A24, XBOOLE_1:1;

A26: ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;

{d} c= D by ZFMISC_1:31;

then A27: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

A28: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13

.= Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

{d} c= D by ZFMISC_1:31;

then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;

A30: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

rng t2 c= D by FINSEQ_1:def 4;

then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;

then A31: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;

rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;

then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;

then A32: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A31, XBOOLE_1:1;

A33: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13

.= Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

let x be object ; :: thesis: ( x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) implies (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x )

A34: dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> = (dom ((dom (G .: (t1,t2))) --> d)) /\ (dom (G .: (t1,t2))) by FUNCT_3:def 7;

assume A35: x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) ; :: thesis: (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x

then x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> by FUNCT_1:11;

then A36: x in dom (G .: (t1,t2)) by A34, XBOOLE_0:def 4;

dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then A37: t1 . x in rng t1 by A22, A35, FUNCT_1:def 3;

A38: dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A25, A29, RELAT_1:27, XBOOLE_1:1

.= Seg n by A33, A30, FUNCT_3:50 ;

then A39: x in dom (H [;] (d,t1)) by A22, A35;

dom t2 = Seg (len t2) by FINSEQ_1:def 3

.= Seg n by CARD_1:def 7 ;

then A40: t2 . x in rng t2 by A22, A35, FUNCT_1:def 3;

dom H = [:D,D:] by FUNCT_2:def 1;

then dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A32, A27, RELAT_1:27, XBOOLE_1:1

.= Seg n by A28, A38, FUNCT_3:50 ;

then A41: x in dom (H [;] (d,t2)) by A22, A35;

(H [;] (d,(G .: (t1,t2)))) . x = H . (d,((G .: (t1,t2)) . x)) by A35, FUNCOP_1:32

.= H . (d,(G . ((t1 . x),(t2 . x)))) by A36, FUNCOP_1:22

.= G . ((H . (d,(t1 . x))),(H . (d,(t2 . x)))) by A23, A37, A26, A40, BINOP_1:11

.= G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x)))) by A39, FUNCOP_1:32

.= G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x)) by A41, FUNCOP_1:32

.= (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x by A22, A20, A35, FUNCOP_1:22 ;

hence (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x ; :: thesis: verum