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:45;
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:71, ZFMISC_1:119;
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:119;
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 FINSEQ_1:def 18 ;
( 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:119;
rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:71;
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:19
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
then dom <:t1,t2:> = Seg n by A4, FUNCT_3:70;
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 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:71, ZFMISC_1:119;
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:19;
then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:119;
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 FINSEQ_1:def 18 ;
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:71, ZFMISC_1:119;
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:19;
then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:119;
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:19
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
{d} c= D by ZFMISC_1:37;
then A16: [:{d},D:] c= [:D,D:] by ZFMISC_1:119;
( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:19, ZFMISC_1:37;
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 FINSEQ_1:def 18 ;
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:46, XBOOLE_1:1
.= Seg n by A7, A18, FUNCT_3:70 ;
{d} c= D by ZFMISC_1:37;
then A20: [:{d},D:] c= [:D,D:] by ZFMISC_1:119;
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:46, XBOOLE_1:1
.= Seg n by A15, A12, FUNCT_3:70 ;
then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A19, FUNCT_3:70;
then A22: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A3, RELAT_1:46;
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:71, ZFMISC_1:119;
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:46;
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:71, ZFMISC_1:119;
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:19;
then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:119;
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:37;
then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:119;
A30: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:19
.= Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
{d} c= D by ZFMISC_1:37;
then A31: [:{d},D:] c= [:D,D:] by ZFMISC_1:119;
A32: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
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:71, ZFMISC_1:119;
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:19;
then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:119;
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:19
.= Seg (len t1) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
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 8;
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:21;
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 FINSEQ_1:def 18 ;
then A39: t1 . x in rng t1 by A24, A37, FUNCT_1:def 5;
A40: dom t2 = Seg (len t2) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
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:46, XBOOLE_1:1
.= Seg n by A35, A32, FUNCT_3:70 ;
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 FINSEQ_1:def 18 ;
then A42: t2 . x in rng t2 by A24, A37, FUNCT_1:def 5;
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:46, XBOOLE_1:1
.= Seg n by A30, A40, FUNCT_3:70 ;
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:42
.= H . d,(G . (t1 . x),(t2 . x)) by A38, FUNCOP_1:28
.= G . (H . d,(t1 . x)),(H . d,(t2 . x)) by A25, A39, A28, A42, BINOP_1:23
.= G . ((H [;] d,t1) . x),(H . d,(t2 . x)) by A41, FUNCOP_1:42
.= G . ((H [;] d,t1) . x),((H [;] d,t2) . x) by A43, FUNCOP_1:42
.= (G .: (H [;] d,t1),(H [;] d,t2)) . x by A21, A24, A22, A37, FUNCOP_1:28 ;
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:9, RELAT_1:46; :: thesis: verum