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

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 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;

hence H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) by A8, A21, A20, RELAT_1:27; :: thesis: verum