let X be set ; :: thesis: for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat 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 Nat; :: thesis: ( n >= 2 implies ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat 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 Nat 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 Nat 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 Def13;
take fs ; :: thesis: ( len fs = n - 1 & ( for p being Nat 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 Nat 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 Nat 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 Nat; :: 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:24;
then ( (- p) + n <= (- 1) + n & (- p) + n >= (- (n - 1)) + n ) by XREAL_1:6;
then n - p = n -' p by 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