let X be set ; :: thesis: for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) )
let n be natural number ; :: thesis: ( n >= 2 implies ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) ) )
assume n >= 2 ; :: thesis: ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) )
then consider fs being FinSequence such that
A1: ( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:((free_magma_seq X) . p),((free_magma_seq X) . (n - p)):] ) & (free_magma_seq X) . n = Union (disjoin fs) ) by Def14;
take fs ; :: thesis: ( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) )
thus len fs = n - 1 by A1; :: thesis: ( ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) )
thus for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] :: thesis: free_magma X,n = Union (disjoin fs)

proof

let p be natural number ; :: thesis: ( p >= 1 & p <= n - 1 implies fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] )
assume A2: ( p >= 1 & p <= n - 1 ) ; :: thesis: fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):]
then ( - p <= - 1 & - p >= - (n - 1) ) by XREAL_1:26;
then A3: ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:8;
n - p = n -' p by A3, XREAL_0:def 2;
hence fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] by A2, A1; :: thesis: verum

end;

thus free_magma X,n = Union (disjoin fs) by A1; :: thesis: verum