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

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;

end;

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;.= A ` by A1, FUNCT_7:119

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

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;.= B ` by A2, FUNCT_7:120

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