let E be set ; :: thesis: for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )
let a be Element of E ^omega ; :: thesis: for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )
let p, q be XFinSequence; :: thesis: ( a = p ^ q implies ( p is Element of E ^omega & q is Element of E ^omega ) )
assume a = p ^ q ; :: thesis: ( p is Element of E ^omega & q is Element of E ^omega )
then ( p is XFinSequence of E & q is XFinSequence of E ) by AFINSQ_1:31;
hence ( p is Element of E ^omega & q is Element of E ^omega ) by AFINSQ_1:def 7; :: thesis: verum