let X be set ; :: thesis: for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
let A, B be Subset of X; :: thesis: Complement (A followed_by B) = (A `) followed_by (B `)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n

per cases ( n = 0 or n > 0 ) by NAT_1:3;

suppose A1: n = 0 ; :: thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n

thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2
.= A ` by A1, FUNCT_7:119
.= ((A `) followed_by (B `)) . n by A1, FUNCT_7:119 ; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: (Complement (A followed_by B)) . n = ((A `) followed_by (B `)) . n

thus (Complement (A followed_by B)) . n = ((A followed_by B) . n) ` by Def2
.= B ` by A2, FUNCT_7:120
.= ((A `) followed_by (B `)) . n by A2, FUNCT_7:120 ; :: thesis: verum

end;

end;