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))) )
A1: H [;] (d,(G .: (t1,t2))) = H [;] (d,(G * <:t1,t2:>)) by FUNCOP_1:def 3
.= H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> by FUNCOP_1:def 5 ;
( 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 A2: 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 A2, XBOOLE_1:1;
then A3: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G by FUNCT_2:def 1;
A4: 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 A5: [:(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 A5, XBOOLE_1:1;
then A6: rng <:t1,t2:> c= dom G by FUNCT_2:def 1;
A7: 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 A4, FUNCT_3:50;
then A8: dom (G * <:t1,t2:>) = Seg n by A6, RELAT_1:27;
then dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:13;
then A9: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A8, 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 A10: 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 A11: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A10, XBOOLE_1:1;
A12: 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 A13: 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 A14: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A13, XBOOLE_1:1;
A15: 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 A16: [:{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 A17: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;
A18: 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 A19: dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A11, A16, RELAT_1:27, XBOOLE_1:1
.= Seg n by A7, A18, FUNCT_3:50 ;
{d} c= D by ZFMISC_1:31;
then A20: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;
A21: G .: ((H [;] (d,t1)),(H [;] (d,t2))) = G .: ((H * <:((dom t1) --> d),t1:>),(H [;] (d,t2))) by FUNCOP_1:def 5
.= G .: ((H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>)) by FUNCOP_1:def 5
.= G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> by FUNCOP_1:def 3 ;
dom H = [:D,D:] by FUNCT_2:def 1;
then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A14, A20, RELAT_1:27, XBOOLE_1:1
.= Seg n by A15, A12, FUNCT_3:50 ;
then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A19, FUNCT_3:50;
then A22: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A3, 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 A17, FUNCT_3:51, ZFMISC_1:96;
then rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] by XBOOLE_1:1;
then A23: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H by FUNCT_2:def 1;
then A24: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A9, RELAT_1:27;
assume A25: H is_distributive_wrt G ; :: thesis: H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
for x being set 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

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 A26: 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 A27: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A26, XBOOLE_1:1;
A28: ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;
{d} c= D by ZFMISC_1:31;
then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A30: 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 A31: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A32: 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 A33: 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 A34: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A33, XBOOLE_1:1;
A35: 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 set ; :: 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 )
A36: 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 A37: 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 (H * <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):>) by A1, FUNCOP_1:def 5;
then x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> by FUNCT_1:11;
then A38: x in dom (G .: (t1,t2)) by A36, XBOOLE_0:def 4;
dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
then A39: t1 . x in rng t1 by A24, A37, FUNCT_1:def 3;
A40: 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 A27, A31, RELAT_1:27, XBOOLE_1:1
.= Seg n by A35, A32, FUNCT_3:50 ;
then A41: x in dom (H [;] (d,t1)) by A24, A37, FUNCOP_1:def 5;
dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
then A42: t2 . x in rng t2 by A24, A37, 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 A34, A29, RELAT_1:27, XBOOLE_1:1
.= Seg n by A30, A40, FUNCT_3:50 ;
then A43: x in dom (H [;] (d,t2)) by A24, A37, FUNCOP_1:def 5;
(H [;] (d,(G .: (t1,t2)))) . x = H . (d,((G .: (t1,t2)) . x)) by A1, A37, FUNCOP_1:32
.= H . (d,(G . ((t1 . x),(t2 . x)))) by A38, FUNCOP_1:22
.= G . ((H . (d,(t1 . x))),(H . (d,(t2 . x)))) by A25, A39, A28, A42, BINOP_1:11
.= G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x)))) by A41, FUNCOP_1:32
.= G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x)) by A43, FUNCOP_1:32
.= (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x by A21, A24, A22, A37, FUNCOP_1:22 ;
hence (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x ; :: thesis: verum

end;

hence H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) by A1, A21, A9, A23, A22, FUNCT_1:2, RELAT_1:27; :: thesis: verum