let n be Nat; :: thesis:
let D be non empty set ; :: thesis:
let H, G be BinOp of D; :: thesis:
let d be Element of D; :: thesis:
let t1, t2 be Element of n -tuples_on D; :: thesis:
assume A1: H is_distributive_wrt G ; :: thesis:
A2: 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 ;
set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;
A3: 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 ;
A4: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n

proof

A5: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
then A6: dom <:t1,t2:> = Seg n by A5, FUNCT_3:70;
( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def 4;
then A7: [:(rng t1),(rng t2):] c= [:D,D:] by ZFMISC_1:119;
rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:71;
then rng <:t1,t2:> c= [:D,D:] by A7, XBOOLE_1:1;
then rng <:t1,t2:> c= dom G by FUNCT_2:def 1;
then A8: dom (G * <:t1,t2:>) = Seg n by A6, RELAT_1:46;
then dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:19;
then A9: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A8, FUNCT_3:70;
rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H

proof

A10: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] by FUNCT_3:71;
( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:19, ZFMISC_1:37;
then A11: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;
A12: rng (G * <:t1,t2:>) c= rng G by RELAT_1:45;
rng G c= D by RELSET_1:12;
then rng (G * <:t1,t2:>) c= D by A12, XBOOLE_1:1;
then [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] by A11, ZFMISC_1:119;
then ( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] & dom H = [:D,D:] ) by A10, FUNCT_2:def 1, XBOOLE_1:1;
hence rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H ; :: thesis:

end;

hence dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A9, RELAT_1:46; :: thesis:

end;

A13: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n

proof

A14: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G

proof

( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H ) by RELAT_1:45;
then A15: ( 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:71, ZFMISC_1:119;
rng H c= D by RELSET_1:12;
then ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):] & [:(rng H),(rng H):] c= [:D,D:] ) by A15, XBOOLE_1:1, ZFMISC_1:119;
then ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:] & dom G = [:D,D:] ) by FUNCT_2:def 1, XBOOLE_1:1;
hence rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G ; :: thesis:

end;

( dom (H * <:((dom t1) --> d),t1:>) = Seg n & dom (H * <:((dom t2) --> d),t2:>) = Seg n )

proof

rng t1 c= D by FINSEQ_1:def 4;
then A16: ( 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:71, ZFMISC_1:119;
rng ((dom t1) --> d) c= {d} by FUNCOP_1:19;
then A17: ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] & [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] ) by A16, XBOOLE_1:1, ZFMISC_1:119;
{d} c= D by ZFMISC_1:37;
then A18: ( rng <:((dom t1) --> d),t1:> c= [:{d},D:] & [:{d},D:] c= [:D,D:] ) by A17, XBOOLE_1:1, ZFMISC_1:119;
A19: dom H = [:D,D:] by FUNCT_2:def 1;
A20: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:19
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A21: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A22: dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A18, A19, RELAT_1:46, XBOOLE_1:1
.= Seg n by A20, A21, FUNCT_3:70 ;
rng t2 c= D by FINSEQ_1:def 4;
then A23: ( 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:71, ZFMISC_1:119;
rng ((dom t2) --> d) c= {d} by FUNCOP_1:19;
then A24: ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] & [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] ) by A23, XBOOLE_1:1, ZFMISC_1:119;
{d} c= D by ZFMISC_1:37;
then A25: ( rng <:((dom t2) --> d),t2:> c= [:{d},D:] & [:{d},D:] c= [:D,D:] ) by A24, XBOOLE_1:1, ZFMISC_1:119;
A26: dom H = [:D,D:] by FUNCT_2:def 1;
A27: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:19
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A28: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A25, A26, RELAT_1:46, XBOOLE_1:1
.= Seg n by A27, A28, FUNCT_3:70 ;
hence ( dom (H * <:((dom t1) --> d),t1:>) = Seg n & dom (H * <:((dom t2) --> d),t2:>) = Seg n ) by A22; :: thesis:

end;

then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by FUNCT_3:70;
hence dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A14, RELAT_1:46; :: thesis:

end;

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

let x be set ; :: thesis:
assume A29: x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) ; :: thesis:
then x in dom (H * <:((dom (G .: t1,t2)) --> d),(G .: t1,t2):>) by A2, FUNCOP_1:def 5;
then A30: x in dom <:((dom (G .: t1,t2)) --> d),(G .: t1,t2):> by FUNCT_1:21;
dom <:((dom (G .: t1,t2)) --> d),(G .: t1,t2):> = (dom ((dom (G .: t1,t2)) --> d)) /\ (dom (G .: t1,t2)) by FUNCT_3:def 8;
then A31: x in dom (G .: t1,t2) by A30, XBOOLE_0:def 4;
A32: ( t1 . x in D & t2 . x in D )

proof

A33: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A34: rng t1 c= D by FINSEQ_1:def 4;
A35: t1 . x in rng t1 by A4, A29, A33, FUNCT_1:def 5;
A36: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A37: rng t2 c= D by FINSEQ_1:def 4;
t2 . x in rng t2 by A4, A29, A36, FUNCT_1:def 5;
hence ( t1 . x in D & t2 . x in D ) by A34, A35, A37; :: thesis:

end;

A38: ( x in dom (H [;] d,t1) & x in dom (H [;] d,t2) )

proof

( dom (H * <:((dom t1) --> d),t1:>) = Seg n & dom (H * <:((dom t2) --> d),t2:>) = Seg n )

proof

rng t1 c= D by FINSEQ_1:def 4;
then A39: ( 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:71, ZFMISC_1:119;
rng ((dom t1) --> d) c= {d} by FUNCOP_1:19;
then A40: ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] & [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] ) by A39, XBOOLE_1:1, ZFMISC_1:119;
{d} c= D by ZFMISC_1:37;
then A41: ( rng <:((dom t1) --> d),t1:> c= [:{d},D:] & [:{d},D:] c= [:D,D:] ) by A40, XBOOLE_1:1, ZFMISC_1:119;
A42: dom H = [:D,D:] by FUNCT_2:def 1;
A43: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:19
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A44: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A45: dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A41, A42, RELAT_1:46, XBOOLE_1:1
.= Seg n by A43, A44, FUNCT_3:70 ;
rng t2 c= D by FINSEQ_1:def 4;
then A46: ( 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:71, ZFMISC_1:119;
rng ((dom t2) --> d) c= {d} by FUNCOP_1:19;
then A47: ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] & [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] ) by A46, XBOOLE_1:1, ZFMISC_1:119;
{d} c= D by ZFMISC_1:37;
then A48: ( rng <:((dom t2) --> d),t2:> c= [:{d},D:] & [:{d},D:] c= [:D,D:] ) by A47, XBOOLE_1:1, ZFMISC_1:119;
A49: dom H = [:D,D:] by FUNCT_2:def 1;
A50: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:19
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
A51: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109 ;
dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A48, A49, RELAT_1:46, XBOOLE_1:1
.= Seg n by A50, A51, FUNCT_3:70 ;
hence ( dom (H * <:((dom t1) --> d),t1:>) = Seg n & dom (H * <:((dom t2) --> d),t2:>) = Seg n ) by A45; :: thesis:

end;

hence ( x in dom (H [;] d,t1) & x in dom (H [;] d,t2) ) by A4, A29, FUNCOP_1:def 5; :: thesis:

end;

(H [;] d,(G .: t1,t2)) . x = H . d,((G .: t1,t2) . x) by A2, A29, FUNCOP_1:42
.= H . d,(G . (t1 . x),(t2 . x)) by A31, FUNCOP_1:28
.= G . (H . d,(t1 . x)),(H . d,(t2 . x)) by A1, A32, BINOP_1:23
.= G . ((H [;] d,t1) . x),(H . d,(t2 . x)) by A38, FUNCOP_1:42
.= G . ((H [;] d,t1) . x),((H [;] d,t2) . x) by A38, FUNCOP_1:42
.= (G .: (H [;] d,t1),(H [;] d,t2)) . x by A3, A4, A13, A29, FUNCOP_1:28 ;
hence (H [;] d,(G .: t1,t2)) . x = (G .: (H [;] d,t1),(H [;] d,t2)) . x ; :: thesis:

end;

hence H [;] d,(G .: t1,t2) = G .: (H [;] d,t1),(H [;] d,t2) by A2, A3, A4, A13, FUNCT_1:9; :: thesis: