deffunc H1( 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) = H1(n,f . n) from NAT_1:sch 11();
A5: Union f c= fin_RelStr_sp
proof
defpred S1[ 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:
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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[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
proof
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:
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;
f . (k + 1) = (f . k) \/ { 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) ) )
}
by A4;
hence S1[k + 1] by ; :: thesis: verum
end;
A11: S1[ 0 ]
proof
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:
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;
for k being Nat holds S1[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;
then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A12: for i being Nat holds f . i c= f . (i + 1)
proof
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 ; :: thesis: verum
end;
A14: for i, j being Element of NAT st i <= j holds
f . i c= f . j
proof
let i, j be Element of NAT ; :: thesis: ( i <= j implies f . i c= f . j )
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A17: S1[k] ; :: thesis: S1[k + 1]
f . (i + k) c= f . ((i + k) + 1) by A12;
hence S1[k + 1] by ; :: thesis: verum
end;
A18: S1[ 0 ] ;
for k being Nat holds S1[k] from hence f . i c= f . j by A15; :: thesis: verum
end;
A19: for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M )
proof
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 ;
consider x1 being object such that
A25: x1 in dom f and
A26: H1 in f . x1 by ;
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 ;
A29: f . x2 c= f . (max (x1,x2)) by ;
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 ;
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 ;
hence ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) by ; :: thesis: verum
end;
for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M
proof
A31: f . 0 c= M by ;
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 ;
then R in f . 0 by ;
hence R in M by A31; :: thesis: verum
end;
then A35: fin_RelStr_sp c= M by ;
then A36: Union f = fin_RelStr_sp by ;
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
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A39: S1[n] ; :: thesis: S1[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;
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 ;
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) ) )

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

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 ;
R1 in fin_RelStr_sp by ;
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 ; :: thesis: verum
end;
end;
end;
A47: S1[ 0 ]
proof
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 ; :: thesis: verum
end;
A49: for n being Nat holds S1[n] from ex y being object st
( y in dom f & X in f . y ) by ;
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 ; :: thesis: verum
end;
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) ) ) ; :: thesis: verum