let Y be non empty set ; :: thesis: for G being Subset of ()
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N

let G be Subset of (); :: thesis: for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N

let A, B, C, D, E, F, J, M, N be a_partition of Y; :: thesis: ( G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N implies CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N )
assume that
A1: G = {A,B,C,D,E,F,J,M,N} and
A2: A <> B and
A3: A <> C and
A4: ( A <> D & A <> E ) and
A5: ( A <> F & A <> J ) and
A6: ( A <> M & A <> N ) and
A7: ( B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N ) and
A8: M <> N ; :: thesis: CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
A9: not B in {A} by ;
( not D in {A} & not E in {A} ) by ;
then A10: {D,E} \ {A} = {D,E} by ZFMISC_1:63;
A11: ( not F in {A} & not J in {A} ) by ;
A12: not C in {A} by ;
G \ {A} = ({A} \/ {B,C,D,E,F,J,M,N}) \ {A} by ;
then A13: G \ {A} = ({A} \ {A}) \/ ({B,C,D,E,F,J,M,N} \ {A}) by XBOOLE_1:42;
A14: ( not M in {A} & not N in {A} ) by ;
{B,C,D,E,F,J,M,N} \ {A} = ({B} \/ {C,D,E,F,J,M,N}) \ {A} by ENUMSET1:22
.= ({B} \ {A}) \/ ({C,D,E,F,J,M,N} \ {A}) by XBOOLE_1:42
.= {B} \/ ({C,D,E,F,J,M,N} \ {A}) by
.= {B} \/ (({C} \/ {D,E,F,J,M,N}) \ {A}) by ENUMSET1:16
.= {B} \/ (({C} \ {A}) \/ ({D,E,F,J,M,N} \ {A})) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J,M,N}) \ {A})) by ENUMSET1:12
.= {B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J,M,N} \ {A}))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ (({F,J} \/ {M,N}) \ {A}))) by
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ (({F,J} \ {A}) \/ ({M,N} \ {A})))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F,J} \/ ({M,N} \ {A})))) by
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ ({M,N} \ {A})))) by
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ {M,N}))) by
.= {B} \/ ({C} \/ ({D,E} \/ {F,J,M,N})) by ENUMSET1:5
.= {B} \/ ({C} \/ {D,E,F,J,M,N}) by ENUMSET1:12
.= {B} \/ {C,D,E,F,J,M,N} by ENUMSET1:16
.= {B,C,D,E,F,J,M,N} by ENUMSET1:22 ;
then A15: G \ {A} = {} \/ {B,C,D,E,F,J,M,N} by ;
A16: '/\' (G \ {A}) c= ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis: x in ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
then consider h being Function, FF being Subset-Family of Y such that
A17: dom h = G \ {A} and
A18: rng h = FF and
A19: for d being set st d in G \ {A} holds
h . d in d and
A20: x = Intersect FF and
A21: x <> {} by BVFUNC_2:def 1;
A22: C in G \ {A} by ;
then A23: h . C in C by A19;
set mbcd = ((h . B) /\ (h . C)) /\ (h . D);
A24: E in G \ {A} by ;
then A25: h . E in rng h by ;
A26: N in G \ {A} by ;
then A27: h . N in rng h by ;
set mbc = (h . B) /\ (h . C);
A28: B in G \ {A} by ;
then h . B in B by A19;
then A29: (h . B) /\ (h . C) in INTERSECTION (B,C) by ;
A30: h . B in rng h by ;
then A31: Intersect FF = meet (rng h) by ;
A32: h . C in rng h by ;
A33: F in G \ {A} by ;
then A34: h . F in rng h by ;
A35: M in G \ {A} by ;
then A36: h . M in rng h by ;
A37: J in G \ {A} by ;
then A38: h . J in rng h by ;
A39: D in G \ {A} by ;
then A40: h . D in rng h by ;
A41: xx c= (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N)
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in xx or p in (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) )
assume A42: p in xx ; :: thesis: p in (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N)
then ( p in h . B & p in h . C ) by ;
then A43: p in (h . B) /\ (h . C) by XBOOLE_0:def 4;
p in h . D by ;
then A44: p in ((h . B) /\ (h . C)) /\ (h . D) by ;
p in h . E by ;
then A45: p in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by ;
p in h . F by ;
then A46: p in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by ;
p in h . J by ;
then A47: p in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) by ;
p in h . M by ;
then A48: p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) by ;
p in h . N by ;
hence p in (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) by ; :: thesis: verum
end;
then ((h . B) /\ (h . C)) /\ (h . D) <> {} by A21;
then A49: not ((h . B) /\ (h . C)) /\ (h . D) in by TARSKI:def 1;
(h . B) /\ (h . C) <> {} by ;
then not (h . B) /\ (h . C) in by TARSKI:def 1;
then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ by ;
then A50: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
h . D in D by ;
then ((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION ((B '/\' C),D) by ;
then ((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ by ;
then A51: ((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D by PARTIT1:def 4;
set mbcdefjm = ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M);
set mbcdefj = (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J);
A52: not x in by ;
set mbcdef = ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F);
set mbcde = (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) <> {} by ;
then A53: not ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in by TARSKI:def 1;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {} by ;
then A54: not (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in by TARSKI:def 1;
(((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) c= xx
proof
A55: rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
then consider x1 being object such that
A56: x1 in dom h and
A57: u = h . x1 by FUNCT_1:def 3;
( x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J or x1 = M or x1 = N ) by ;
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)} by ; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) or p in xx )
assume A58: p in (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) ; :: thesis: p in xx
then A59: p in h . N by XBOOLE_0:def 4;
A60: p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) by ;
then A61: p in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) by XBOOLE_0:def 4;
then A62: p in h . J by XBOOLE_0:def 4;
A63: p in h . M by ;
A64: p in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by ;
then A65: p in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by XBOOLE_0:def 4;
then A66: p in h . E by XBOOLE_0:def 4;
A67: p in ((h . B) /\ (h . C)) /\ (h . D) by ;
then A68: p in h . D by XBOOLE_0:def 4;
p in (h . B) /\ (h . C) by ;
then A69: ( p in h . B & p in h . C ) by XBOOLE_0:def 4;
p in h . F by ;
then for y being set st y in rng h holds
p in y by ;
hence p in xx by ; :: thesis: verum
end;
then A70: (((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)) /\ (h . N) = x by ;
h . E in E by ;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION (((B '/\' C) '/\' D),E) by ;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION (((B '/\' C) '/\' D),E)) \ by ;
then A71: (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E by PARTIT1:def 4;
h . F in F by ;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F) by ;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ by ;
then A72: ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (((B '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:def 4;
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) <> {} by ;
then A73: not (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in by TARSKI:def 1;
h . J in J by ;
then (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J) by ;
then (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ by ;
then A74: (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by PARTIT1:def 4;
((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) <> {} by ;
then A75: not ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) in by TARSKI:def 1;
h . M in M by ;
then ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) in INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M) by ;
then ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) in (INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M)) \ by ;
then A76: ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:def 4;
h . N in N by ;
then x in INTERSECTION (((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M),N) by ;
then x in (INTERSECTION (((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M),N)) \ by ;
hence x in ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N by PARTIT1:def 4; :: thesis: verum
end;
A77: ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N c= '/\' (G \ {A})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A78: x in ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N ; :: thesis: x in '/\' (G \ {A})
then A79: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M),N)) \ by ;
then consider bcdefjm, n being set such that
A80: bcdefjm in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M and
A81: n in N and
A82: x = bcdefjm /\ n by SETFAM_1:def 5;
bcdefjm in (INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M)) \ by ;
then consider bcdefj, m being set such that
A83: bcdefj in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J and
A84: m in M and
A85: bcdefjm = bcdefj /\ m by SETFAM_1:def 5;
bcdefj in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ by ;
then consider bcdef, j being set such that
A86: bcdef in (((B '/\' C) '/\' D) '/\' E) '/\' F and
A87: j in J and
A88: bcdefj = bcdef /\ j by SETFAM_1:def 5;
bcdef in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ by ;
then consider bcde, f being set such that
A89: bcde in ((B '/\' C) '/\' D) '/\' E and
A90: f in F and
A91: bcdef = bcde /\ f by SETFAM_1:def 5;
bcde in (INTERSECTION (((B '/\' C) '/\' D),E)) \ by ;
then consider bcd, e being set such that
A92: bcd in (B '/\' C) '/\' D and
A93: e in E and
A94: bcde = bcd /\ e by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ by ;
then consider bc, d being set such that
A95: bc in B '/\' C and
A96: d in D and
A97: bcd = bc /\ d by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ by ;
then consider b, c being set such that
A98: b in B and
A99: c in C and
A100: bc = b /\ c by SETFAM_1:def 5;
set h = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n);
A101: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N = n by FUNCT_7:94;
A102: dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) = {N,B,C,D,E,F,J,M} by Th63
.= {N} \/ {B,C,D,E,F,J,M} by ENUMSET1:22
.= {B,C,D,E,F,J,M,N} by ENUMSET1:28 ;
then A103: C in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ENUMSET1:def 6;
A104: for p being set st p in G \ {A} holds
((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . p in p
proof
let p be set ; :: thesis: ( p in G \ {A} implies ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . p in p )
assume p in G \ {A} ; :: thesis: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . p in p
then ( p = B or p = C or p = D or p = E or p = F or p = J or p = M or p = N ) by ;
hence ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . p in p by A7, A8, A81, A84, A87, A90, A93, A96, A98, A99, Lm1, Th62, FUNCT_7:94; :: thesis: verum
end;
A105: D in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
then A106: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D in rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by FUNCT_1:def 3;
A107: N in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
A108: M in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
A109: J in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
A110: F in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
A111: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B = b by ;
A112: rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) c= {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) or t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} )
assume t in rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
then consider x1 being object such that
A113: x1 in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) and
A114: t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = D & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = B & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = C & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = E & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = F & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = J & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = M & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) or ( x1 = N & t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ) )
per cases ( x1 = D or x1 = B or x1 = C or x1 = E or x1 = F or x1 = J or x1 = M or x1 = N ) by ;
case x1 = D ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = B ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = C ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = E ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = F ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = J ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = M ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
case x1 = N ; :: thesis: t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)}
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} by ; :: thesis: verum
end;
end;
end;
hence t in {(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N)} ; :: thesis: verum
end;
A115: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J = j by ;
A116: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F = f by ;
A117: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M = m by ;
A118: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E = e by ;
A119: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C = c by ;
A120: ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D = d by ;
rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) or t in bool Y )
assume A121: t in rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) ; :: thesis: t in bool Y
now :: thesis: ( ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M & t in bool Y ) or ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N & t in bool Y ) )
per cases ( t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M or t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N ) by ;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . F ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . J ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . M ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
case t = ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . N ; :: thesis: t in bool Y
hence t in bool Y by ; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider FF = rng ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) as Subset-Family of Y ;
A122: E in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
A123: B in dom ((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) by ;
{(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . B),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . C),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . D),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) +* (N .--> n)) . E),(((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E