deffunc H_{1}( set , set ) -> set = $2 \/ { x where x is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in $2 & R2 in $2 & ( x = union_of (R1,R2) or x = sum_of (R1,R2) ) ) } ;

set Y = fin_RelStr_sp ;

let X be set ; :: thesis: ( not X in fin_RelStr_sp or X is 1 -element strict RelStr or ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )

assume A1: X in fin_RelStr_sp ; :: thesis: ( X is 1 -element strict RelStr or ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )

consider f being Function such that

A2: dom f = NAT and

A3: f . 0 = { x where x is Element of fin_RelStr_sp : x is trivial RelStr } and

A4: for n being Nat holds f . (n + 1) = H_{1}(n,f . n)
from NAT_1:sch 11();

A5: Union f c= fin_RelStr_sp

A12: for i being Nat holds f . i c= f . (i + 1)

f . i c= f . j

( union_of (H1,H2) in M & sum_of (H1,H2) in M )

R in M

then A36: Union f = fin_RelStr_sp by A5, XBOOLE_0:def 10;

assume A37: X is not 1 -element strict RelStr ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) ; :: thesis: verum

( the carrier of R1 misses the carrier of R2 & R1 in $2 & R2 in $2 & ( x = union_of (R1,R2) or x = sum_of (R1,R2) ) ) } ;

set Y = fin_RelStr_sp ;

let X be set ; :: thesis: ( not X in fin_RelStr_sp or X is 1 -element strict RelStr or ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )

assume A1: X in fin_RelStr_sp ; :: thesis: ( X is 1 -element strict RelStr or ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )

consider f being Function such that

A2: dom f = NAT and

A3: f . 0 = { x where x is Element of fin_RelStr_sp : x is trivial RelStr } and

A4: for n being Nat holds f . (n + 1) = H

A5: Union f c= fin_RelStr_sp

proof

then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
defpred S_{1}[ Nat] means f . $1 c= fin_RelStr_sp ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union f or y in fin_RelStr_sp )

assume y in Union f ; :: thesis: y in fin_RelStr_sp

then consider x being object such that

A6: x in dom f and

A7: y in f . x by CARD_5:2;

reconsider x = x as Element of NAT by A2, A6;

A8: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A11, A8);

then f . x c= fin_RelStr_sp ;

hence y in fin_RelStr_sp by A7; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union f or y in fin_RelStr_sp )

assume y in Union f ; :: thesis: y in fin_RelStr_sp

then consider x being object such that

A6: x in dom f and

A7: y in f . x by CARD_5:2;

reconsider x = x as Element of NAT by A2, A6;

A8: for k being Nat st S

S

proof

A11:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A9: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A10: { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } c= fin_RelStr_sp

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

hence S_{1}[k + 1]
by A9, A10, XBOOLE_1:8; :: thesis: verum

end;assume A9: S

A10: { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } c= fin_RelStr_sp

proof

f . (k + 1) = (f . k) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } or x in fin_RelStr_sp )

set S = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

assume x in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ; :: thesis: x in fin_RelStr_sp

then ex a being Element of fin_RelStr_sp st

( x = a & ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;

hence x in fin_RelStr_sp ; :: thesis: verum

end;( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } or x in fin_RelStr_sp )

set S = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

assume x in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ; :: thesis: x in fin_RelStr_sp

then ex a being Element of fin_RelStr_sp st

( x = a & ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;

hence x in fin_RelStr_sp ; :: thesis: verum

( the carrier of R1 misses the carrier of R2 & R1 in f . k & R2 in f . k & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

hence S

proof

for k being Nat holds S
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f . 0 or y in fin_RelStr_sp )

assume y in f . 0 ; :: thesis: y in fin_RelStr_sp

then ex a being Element of fin_RelStr_sp st

( y = a & a is trivial RelStr ) by A3;

hence y in fin_RelStr_sp ; :: thesis: verum

end;assume y in f . 0 ; :: thesis: y in fin_RelStr_sp

then ex a being Element of fin_RelStr_sp st

( y = a & a is trivial RelStr ) by A3;

hence y in fin_RelStr_sp ; :: thesis: verum

then f . x c= fin_RelStr_sp ;

hence y in fin_RelStr_sp by A7; :: thesis: verum

A12: for i being Nat holds f . i c= f . (i + 1)

proof

A14:
for i, j being Element of NAT st i <= j holds
let i be Nat; :: thesis: f . i c= f . (i + 1)

A13: f . (i + 1) = (f . i) \/ { b where b is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . i & R2 in f . i & ( b = union_of (R1,R2) or b = sum_of (R1,R2) ) ) } by A4;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . i or x in f . (i + 1) )

assume x in f . i ; :: thesis: x in f . (i + 1)

hence x in f . (i + 1) by A13, XBOOLE_0:def 3; :: thesis: verum

end;A13: f . (i + 1) = (f . i) \/ { b where b is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . i & R2 in f . i & ( b = union_of (R1,R2) or b = sum_of (R1,R2) ) ) } by A4;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . i or x in f . (i + 1) )

assume x in f . i ; :: thesis: x in f . (i + 1)

hence x in f . (i + 1) by A13, XBOOLE_0:def 3; :: thesis: verum

f . i c= f . j

proof

A19:
for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
let i, j be Element of NAT ; :: thesis: ( i <= j implies f . i c= f . j )

defpred S_{1}[ Nat] means f . i c= f . (i + $1);

assume i <= j ; :: thesis: f . i c= f . j

then A15: ex k being Nat st j = i + k by NAT_1:10;

A16: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A18, A16);

hence f . i c= f . j by A15; :: thesis: verum

end;defpred S

assume i <= j ; :: thesis: f . i c= f . j

then A15: ex k being Nat st j = i + k by NAT_1:10;

A16: for k being Nat st S

S

proof

A18:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A17: S_{1}[k]
; :: thesis: S_{1}[k + 1]

f . (i + k) c= f . ((i + k) + 1) by A12;

hence S_{1}[k + 1]
by A17, XBOOLE_1:1; :: thesis: verum

end;assume A17: S

f . (i + k) c= f . ((i + k) + 1) by A12;

hence S

for k being Nat holds S

hence f . i c= f . j by A15; :: thesis: verum

( union_of (H1,H2) in M & sum_of (H1,H2) in M )

proof

for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
let H1, H2 be strict RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M implies ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) )

assume that

A20: the carrier of H1 misses the carrier of H2 and

A21: H1 in M and

A22: H2 in M ; :: thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )

consider x2 being object such that

A23: x2 in dom f and

A24: H2 in f . x2 by A22, CARD_5:2;

consider x1 being object such that

A25: x1 in dom f and

A26: H1 in f . x1 by A21, CARD_5:2;

reconsider x1 = x1, x2 = x2 as Element of NAT by A2, A25, A23;

set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

A27: f . ((max (x1,x2)) + 1) = (f . (max (x1,x2))) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

A28: f . x1 c= f . (max (x1,x2)) by A14, XXREAL_0:25;

A29: f . x2 c= f . (max (x1,x2)) by A14, XXREAL_0:25;

sum_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

then sum_of (H1,H2) in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A20, A26, A24, A28, A29;

then A30: sum_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;

union_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

then union_of (H1,H2) in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A20, A26, A24, A28, A29;

then union_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;

hence ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) by A2, A30, CARD_5:2; :: thesis: verum

end;assume that

A20: the carrier of H1 misses the carrier of H2 and

A21: H1 in M and

A22: H2 in M ; :: thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )

consider x2 being object such that

A23: x2 in dom f and

A24: H2 in f . x2 by A22, CARD_5:2;

consider x1 being object such that

A25: x1 in dom f and

A26: H1 in f . x1 by A21, CARD_5:2;

reconsider x1 = x1, x2 = x2 as Element of NAT by A2, A25, A23;

set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

A27: f . ((max (x1,x2)) + 1) = (f . (max (x1,x2))) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

A28: f . x1 c= f . (max (x1,x2)) by A14, XXREAL_0:25;

A29: f . x2 c= f . (max (x1,x2)) by A14, XXREAL_0:25;

sum_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

then sum_of (H1,H2) in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A20, A26, A24, A28, A29;

then A30: sum_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;

union_of (H1,H2) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

then union_of (H1,H2) in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . (max (x1,x2)) & R2 in f . (max (x1,x2)) & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A20, A26, A24, A28, A29;

then union_of (H1,H2) in f . ((max (x1,x2)) + 1) by A27, XBOOLE_0:def 3;

hence ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) by A2, A30, CARD_5:2; :: thesis: verum

R in M

proof

then A35:
fin_RelStr_sp c= M
by A19, Def5;
A31:
f . 0 c= M
by A2, CARD_5:2;

let R be strict RelStr ; :: thesis: ( the carrier of R is 1 -element & the carrier of R in FinSETS implies R in M )

assume that

A32: the carrier of R is 1 -element and

A33: the carrier of R in FinSETS ; :: thesis: R in M

A34: R is trivial RelStr by A32;

R is Element of fin_RelStr_sp by A32, A33, Def5;

then R in f . 0 by A3, A34;

hence R in M by A31; :: thesis: verum

end;let R be strict RelStr ; :: thesis: ( the carrier of R is 1 -element & the carrier of R in FinSETS implies R in M )

assume that

A32: the carrier of R is 1 -element and

A33: the carrier of R in FinSETS ; :: thesis: R in M

A34: R is trivial RelStr by A32;

R is Element of fin_RelStr_sp by A32, A33, Def5;

then R in f . 0 by A3, A34;

hence R in M by A31; :: thesis: verum

then A36: Union f = fin_RelStr_sp by A5, XBOOLE_0:def 10;

assume A37: X is not 1 -element strict RelStr ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

proof

hence
ex H1, H2 being strict RelStr st
defpred S_{1}[ Nat] means ( X in f . $1 implies ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) );

A38: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A47, A38);

ex y being object st

( y in dom f & X in f . y ) by A1, A35, CARD_5:2;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A2, A49; :: thesis: verum

end;( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) );

A38: for k being Nat st S

S

proof

A47:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A39: S_{1}[n]
; :: thesis: S_{1}[n + 1]

set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

assume A40: X in f . (n + 1) ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A41: f . (n + 1) = (f . n) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

end;assume A39: S

set W = { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ;

assume A40: X in f . (n + 1) ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A41: f . (n + 1) = (f . n) \/ { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } by A4;

per cases
( X in f . n or X in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ) by A40, A41, XBOOLE_0:def 3;

end;

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ) by A40, A41, XBOOLE_0:def 3;

suppose
X in f . n
; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

hence
ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A39; :: thesis: verum

end;( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A39; :: thesis: verum

suppose
X in { a where a is Element of fin_RelStr_sp : ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) } ; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

then
ex a being Element of fin_RelStr_sp st

( a = X & ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;

then consider R1, R2 being strict RelStr such that

A42: the carrier of R1 misses the carrier of R2 and

A43: R1 in f . n and

A44: R2 in f . n and

A45: ( X = union_of (R1,R2) or X = sum_of (R1,R2) ) ;

A46: R2 in fin_RelStr_sp by A2, A36, A44, CARD_5:2;

R1 in fin_RelStr_sp by A2, A36, A43, CARD_5:2;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A42, A45, A46; :: thesis: verum

end;( a = X & ex R1, R2 being strict RelStr st

( the carrier of R1 misses the carrier of R2 & R1 in f . n & R2 in f . n & ( a = union_of (R1,R2) or a = sum_of (R1,R2) ) ) ) ;

then consider R1, R2 being strict RelStr such that

A42: the carrier of R1 misses the carrier of R2 and

A43: R1 in f . n and

A44: R2 in f . n and

A45: ( X = union_of (R1,R2) or X = sum_of (R1,R2) ) ;

A46: R2 in fin_RelStr_sp by A2, A36, A44, CARD_5:2;

R1 in fin_RelStr_sp by A2, A36, A43, CARD_5:2;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A42, A45, A46; :: thesis: verum

proof

A49:
for n being Nat holds S
assume
X in f . 0
; :: thesis: ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

then consider a being Element of fin_RelStr_sp such that

A48: ( X = a & a is trivial RelStr ) by A3;

a is non empty strict RelStr by Th4;

then a is non empty trivial strict RelStr by A48;

then reconsider a = a as non empty trivial strict RelStr ;

a is 1 -element strict RelStr ;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A37, A48; :: thesis: verum

end;( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) )

then consider a being Element of fin_RelStr_sp such that

A48: ( X = a & a is trivial RelStr ) by A3;

a is non empty strict RelStr by Th4;

then a is non empty trivial strict RelStr by A48;

then reconsider a = a as non empty trivial strict RelStr ;

a is 1 -element strict RelStr ;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A37, A48; :: thesis: verum

ex y being object st

( y in dom f & X in f . y ) by A1, A35, CARD_5:2;

hence ex H1, H2 being strict RelStr st

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) by A2, A49; :: thesis: verum

( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) ; :: thesis: verum