let n be Nat; :: thesis: for X being set

for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

let X be set ; :: thesis: for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

let A1 be SetSequence of X; :: thesis: A1 . n c= (Partial_Union A1) . n

for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

let X be set ; :: thesis: for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

let A1 be SetSequence of X; :: thesis: A1 . n c= (Partial_Union A1) . n

per cases
( n = 0 or ex k being Nat st n = k + 1 )
by NAT_1:6;

end;

suppose
ex k being Nat st n = k + 1
; :: thesis: A1 . n c= (Partial_Union A1) . n

then consider k being Nat such that

A1: n = k + 1 ;

(Partial_Union A1) . (k + 1) = ((Partial_Union A1) . k) \/ (A1 . (k + 1)) by Def2;

hence A1 . n c= (Partial_Union A1) . n by A1, XBOOLE_1:7; :: thesis: verum

end;A1: n = k + 1 ;

(Partial_Union A1) . (k + 1) = ((Partial_Union A1) . k) \/ (A1 . (k + 1)) by Def2;

hence A1 . n c= (Partial_Union A1) . n by A1, XBOOLE_1:7; :: thesis: verum