let X be set ; :: thesis: for p, p1, p2 being FinSequence st (p ^ p1) ^ p2 is X -valued holds
( p2 is X -valued & p1 is X -valued & p is X -valued )
let p, p1, p2 be FinSequence; :: thesis: ( (p ^ p1) ^ p2 is X -valued implies ( p2 is X -valued & p1 is X -valued & p is X -valued ) )
set q = (p ^ p1) ^ p2;
assume (p ^ p1) ^ p2 is X -valued ; :: thesis: ( p2 is X -valued & p1 is X -valued & p is X -valued )
then ( rng ((p ^ p1) ^ p2) c= X & rng (p ^ p1) c= rng ((p ^ p1) ^ p2) & rng p2 c= rng ((p ^ p1) ^ p2) ) by FINSEQ_1:29, FINSEQ_1:30;
then ( rng p2 c= X & rng p c= rng (p ^ p1) & rng p1 c= rng (p ^ p1) & rng (p ^ p1) c= X ) by FINSEQ_1:29, FINSEQ_1:30;
hence ( p2 is X -valued & p1 is X -valued & p is X -valued ) by XBOOLE_1:1; :: thesis: verum